Document Open Access Logo

Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory

Author Gilles Dowek

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.109.pdf
  • Filesize: 472 kB
  • 14 pages

Document Identifiers

Author Details

Gilles Dowek

Cite As Get BibTex

Gilles Dowek. Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 109:1-109:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ICALP.2017.109

Abstract

We define a notion of model for the lambda Pi-calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction terminates in the lambda Pi-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions.

Subject Classification

Keywords
  • model
  • proof reduction
  • Simple type theory
  • Calculus of constructions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. Dedukti: a logical framework based on the lambda-Pi-calculus modulo theory. http://www.lsv.ens-cachan.fr/~dowek/Publi/ expressing.pdf, 2016. Google Scholar
  2. A. Assaf, G. Dowek, J.-P. Jouannaud, and J. Liu. Untyped confluence in dependent type theories. Submitted to publication, 2017. Google Scholar
  3. A. Bauer, G. Gilbert, P. Haselwarter, M. Pretnar, and Ch. A. Stone. Design and implementation of the andromeda proof assistant. Types, 2016. Google Scholar
  4. F. Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1):37-92, 2005. Google Scholar
  5. A. Brunel, O. Hermant, and C. Houtmann. Orthogonality and boolean algebras for deduction modulo. In L. Ong, editor, Typed Lambda Calculus and Applications, volume 6690 of Lecture Notes in Computer Science, pages 76-90. Springer-Verlag, 2011. Google Scholar
  6. H. Cirstea, L. Liquori, and B. Wack. Rewriting calculus with fixpoints: Untyped and first-order systems. In Types, volume 3085 of Lectures Notes in Computer Science. Springer-Verlag, 2003. Google Scholar
  7. T. Coquand and G. Huet. The calculus of constructions. Information and Computation, pages 95-120, 1988. Google Scholar
  8. D. Cousineau and G. Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In S. Ronchi Della Rocca, editor, Typed lambda calculi and applications, volume 4583 of Lecture Notes in Computer Science, pages 102-117. Springer-Verlag, 2007. Google Scholar
  9. G. Dowek. Truth values algebras and proof normalization. In Th. Altenkirch and C. McBride, editors, Types for proofs and programs, volume 4502 of Lecture Notes in Computer Science, pages 110-124. Springer-Verlag, 2007. Google Scholar
  10. G. Dowek, Th. Hardin, and C. Kirchner. Hol-lambda-sigma: an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science, 11:1-25, 2001. Google Scholar
  11. G. Dowek, Th. Hardin, and C. Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31:33-72, 2003. Google Scholar
  12. G. Dowek and B. Werner. Proof normalization modulo. The Journal of Symbolic Logic, 68(4):1289-1316, 2003. Google Scholar
  13. S. Foster and G. Struth. Integrating an automated theorem prover into agda. In M. Bobaru, K. Havelund, G.J. Holzmann, and R. Joshi, editors, NASA Formal Methods, volume 6617 of Lecture Notes in Computer Science. Springer-Verlag, 2011. Google Scholar
  14. H. Geuvers. A short and flexible proof of strong normalization for the calculus of constructions. In P. Dybjer, , B. Nordström, and J. Smith, editors, Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science, pages 14-38. Springer-Verlag, 1995. Google Scholar
  15. J. Y. Girard. Interprétation Fonctionnelle et Élimination des Coupures dans l'Arithmétique d'Ordre Supérieur. PhD thesis, Université de Paris VII, 1972. Google Scholar
  16. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. Google Scholar
  17. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  18. P.-A. Melliès and B. Werner. A generic normalisation proof for pure type systems. In E. Giménez and Ch. Paulin-Mohring, editors, Types for Proofs and Programs, volume 1512 of Lecture Notes in Computer Science, pages 254-276. Springer-Verlag, 1998. Google Scholar
  19. A. Miquel and B. Werner. The not so simple proof-irrelevant model of CC. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, pages 240-258. Springer-Verlag, 2003. Google Scholar
  20. Q. H. Nguyen, C. Kirchner, and H. Kirchner. External rewriting for skeptical proof assistants. Journal of Automated Reasoning, 29(309), 2002. Google Scholar
  21. B. Nordström, K. Petersson, and J. M. Smith. Martin-löf’s type theory. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 1-37. Clarendon Press, 2000. Google Scholar
  22. M. Parigot. Proofs of strong normalization for second order classical natural deduction. In Logic in Computer Science, pages 39-46, 1993. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact