Dialectica interpretation with fine computational control

DOI10.1007/978-3-642-03073-4_48MaRDI QIDQ3576085zbMATH OpenOpenAlexFDO

Authors Trifon Trifonov

Publication date 28 July 2010

Published in Mathematical Theory and Computational Practice (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03073-4_48

Mathematics Subject Classification ID

Logic in computer science (03B70) Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50)

Recommendations

• Dialectica interpretation with marked counterexamples
• Quasi-linear Dialectica Extraction
• Computer Science Logic
• Analysis of methods for extraction of programs from non-constructive proofs.
• Light Dialectica revisited

Cites work

• Dialectica interpretation of well-founded induction
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• Hybrid Functional Interpretations
• Light Dialectica revisited
• 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
• Uniform Heyting arithmetic

Cited in

(4)

• Quasi-linear Dialectica Extraction
• Dialectica interpretation with marked counterexamples
• Modal functional (``Dialectica) interpretation
• Light Dialectica revisited

This page was built for publication: Dialectica interpretation with fine computational control

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3576085)