Light Dialectica revisited

DOI10.1016/j.apal.2010.04.008zbMath1223.03040arXiv1212.0020OpenAlexW2052037434MaRDI QIDQ636373

Mircea-Dan Hernest, Trifon Trifonov

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1212.0020

zbMATH Keywords

functional interpretationsautomated program synthesiscomputational content of proofslight Dialectica interpretationlight/uniform quantifiersprogram extraction from proofs

Mathematics Subject Classification ID

Logic in computer science (03B70) Functionals in proof theory (03F10) Complexity of proofs (03F20)

Related Items

Unnamed Item, Dialectica Interpretation with Fine Computational Control

Cites Work

• Unnamed Item
• Unnamed Item
• Linear logic
• Unifying functional interpretations
• Uniform Heyting arithmetic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Dialectica interpretation of well-founded induction
• Hybrid Functional Interpretations
• Dialectica Interpretation with Fine Computational Control
• Computational Interpretations of Classical Linear Logic
• Computer Science Logic
• A note on Spector's quantifier-free rule of extensionality
• Refined program extraction from classical proofs