skip to main content
10.1145/2603088.2603094acmconferencesArticle/Chapter ViewAbstractPublication PageslicsConference Proceedingsconference-collections
research-article

A functional functional interpretation

Published:14 July 2014Publication History

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.

References

  1. 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 ScholarGoogle Scholar
  2. Thierry Coquand. An analysis of Girard's paradox. In LICS, pages 227--236. IEEE Computer Society, 1986.Google ScholarGoogle Scholar
  3. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  4. 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 ScholarGoogle Scholar
  5. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1--102, 1987. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Jean-Yves Girard. The Blind Spot: Lectures on Logic. European Mathematical Society, 2011.Google ScholarGoogle ScholarCross RefCross Ref
  7. Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12:280--287, 1958.Google ScholarGoogle ScholarCross RefCross Ref
  8. Hugo Herbelin. An intuitionistic logic that proves Markov's principle. Logic in Computer Science, Symposium on, 0:50--56, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. J. M. E. Hyland. Proof theory in the abstract. Ann. Pure Appl. Logic, 114(1-3):43--78, 2002.Google ScholarGoogle ScholarCross RefCross Ref
  10. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theor. Comput. Sci., 294(1/2):183--231, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Jean-Louis Krivine. Dependent choice, 'quote' and the clock. Theor. Comput. Sci., 308(1-3):259--276, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Zhaohui Luo. ECC, an extended calculus of constructions. In LICS, pages 386--395. IEEE Computer Society, 1989. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Alexandre Miquel. Forcing as a program transformation. In LICS, pages 197--206. IEEE Computer Society, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Univ. Paris Diderot, December 2013.Google ScholarGoogle Scholar
  15. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  16. Paulo Oliva. Unifying functional interpretations. Notre Dame Journal of Formal Logic, 47(2):263--290, 04 2006.Google ScholarGoogle ScholarCross RefCross Ref
  17. Thomas Streicher and Ulrich Kohlenbach. Shoenfield is Gödel after Krivine. Math. Log. Q., 53(2):176--179, 2007.Google ScholarGoogle ScholarCross RefCross Ref

Index Terms

  1. A functional functional interpretation

      Recommendations

      Comments

      Login options

      Check if you have access through your login credentials or your institution to get full access on this article.

      Sign in
      • Published in

        cover image ACM Conferences
        CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
        July 2014
        764 pages
        ISBN:9781450328869
        DOI:10.1145/2603088
        • Program Chairs:
        • Thomas Henzinger,
        • Dale Miller

        Copyright © 2014 ACM

        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        • Published: 14 July 2014

        Permissions

        Request permissions about this article.

        Request Permissions

        Check for updates

        Qualifiers

        • research-article

        Acceptance Rates

        CSL-LICS '14 Paper Acceptance Rate74of212submissions,35%Overall Acceptance Rate143of386submissions,37%

      PDF Format

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader