ABSTRACT
In this paper, we present a modern reformulation of the Dialectica interpretation based on the linearized version of de Paiva. Contrarily to Gödel's original translation which translated HA into system T, our presentation applies on untyped λ-terms and features nicer proof-theoretical properties.
In the Curry-Howard perspective, we show that the computational behaviour of this translation can be accurately described by the explicit stack manipulation of the Krivine abstract machine, thus giving it a direct-style operational explanation.
Finally, we give direct evidence that supports the fact our presentation is quite relevant, by showing that we can apply it to the dependently-typed calculus of constructions with universes CCω almost without any adaptation. This answers the question of the validity of Dialectica-like constructions in a dependent setting.
- Jeremy Avigad and Solomon Feferman. Gödel's functional ('dialectica') interpretation. In Samuel R. Buss, editor, Handbook of Proof Theory, pages 337--405. Elsevier Science Publishers, Amsterdam, 1998.Google Scholar
- Thierry Coquand. An analysis of Girard's paradox. In LICS, pages 227--236. IEEE Computer Society, 1986.Google Scholar
- Valeria de Paiva. A dialectica-like model of linear logic. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science, pages 341--356. Springer, 1989. Google ScholarDigital Library
- Justus Diller. Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen. Archiv für mathematische Logik und Grundlagenforschung, 16(1-2):49--66, 1974.Google Scholar
- Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1--102, 1987. Google ScholarDigital Library
- Jean-Yves Girard. The Blind Spot: Lectures on Logic. European Mathematical Society, 2011.Google ScholarCross Ref
- Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12:280--287, 1958.Google ScholarCross Ref
- Hugo Herbelin. An intuitionistic logic that proves Markov's principle. Logic in Computer Science, Symposium on, 0:50--56, 2010. Google ScholarDigital Library
- J. M. E. Hyland. Proof theory in the abstract. Ann. Pure Appl. Logic, 114(1-3):43--78, 2002.Google ScholarCross Ref
- Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theor. Comput. Sci., 294(1/2):183--231, 2003. Google ScholarDigital Library
- Jean-Louis Krivine. Dependent choice, 'quote' and the clock. Theor. Comput. Sci., 308(1-3):259--276, 2003. Google ScholarDigital Library
- Zhaohui Luo. ECC, an extended calculus of constructions. In LICS, pages 386--395. IEEE Computer Society, 1989. Google ScholarDigital Library
- Alexandre Miquel. Forcing as a program transformation. In LICS, pages 197--206. IEEE Computer Society, 2011. Google ScholarDigital Library
- Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Univ. Paris Diderot, December 2013.Google Scholar
- Guillaume Munch-Maccagnoni. Formulae-as-types for an involutive negation. In Proceedings of the joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS), 2014. Google ScholarDigital Library
- Paulo Oliva. Unifying functional interpretations. Notre Dame Journal of Formal Logic, 47(2):263--290, 04 2006.Google ScholarCross Ref
- Thomas Streicher and Ulrich Kohlenbach. Shoenfield is Gödel after Krivine. Math. Log. Q., 53(2):176--179, 2007.Google ScholarCross Ref
Index Terms
A functional functional interpretation
Recommendations
A sequent calculus with dependent types for classical arithmetic
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceIn a recent paper [11], Herbelin developed dPAω, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of it components. ...
The Linear Logical Abstract Machine
We derive an abstract machine from the Curry-Howard correspondence with a sequent calculus presentation of Intuitionistic Propositional Linear Logic. The states of the register based abstract machine comprise a low-level code block, a register bank and ...
A herbrandized functional interpretation of classical first-order logic
AbstractWe introduce a new typed combinatory calculus with a type constructor that, to each type , associates the star type of the nonempty finite subsets of elements of type . We prove that this calculus enjoys the properties of strong normalization ...
Comments