Dialectica interpretation with marked counterexamples

MaRDI QIDQ4964700zbMATH OpenFDO

Authors Trifon Trifonov

Publication date 3 March 2021

Full work available at URL https://arxiv.org/abs/1101.5446, http://eptcs.web.cse.unsw.edu.au/paper.cgi?CLaC10.8

Mathematics Subject Classification ID

Logic in computer science (03B70) Functionals in proof theory (03F10) Complexity of proofs (03F20) Relative consistency and interpretations (03F25)

Recommendations

• Quasi-linear Dialectica Extraction
• Analysis of methods for extraction of programs from non-constructive proofs.
• Computer Science Logic
• Dialectica interpretation with fine computational control
• A complexity analysis of functional interpretations

Cited in

(7)

• Dialectica logical principles
• Light Dialectica program extraction from a classical Fibonacci proof
• Analysis of methods for extraction of programs from non-constructive proofs.
• Dialectica interpretation of well-founded induction
• Dialectica interpretation with fine computational control
• A functional interpretation with state
• Computer Science Logic

This page was built for publication: Dialectica interpretation with marked counterexamples

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