2 papers
cs.LO2012
Modal Functional (Dialectica) Interpretation
Dan Hernest, Trifon Trifonov
We adapt our light Dialectica interpretation to usual and light modal formulas (with universal quantification on boolean and natural variables) and prove it sound for a non-standar…
cs.LO2011
Dialectica Interpretation with Marked Counterexamples
Trifon Trifonov
Goedel's functional "Dialectica" interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witness…