Abstract
The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calculus modulo. We show in this paper that this simple extension is surprisingly expressive and, in particular, that all functional Pure Type Systems, such as the system F, or the Calculus of Constructions, can be embedded in it. And, moreover, that this embedding is conservative under termination hypothesis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, pp. 117–309. Oxford University Press, Oxford (1992)
Berardi, S.: Towards a mathematical analysis of the Coquand-Huet Calculus of Constructions and the other systems in Barendregt’s cube (manuscript 1988)
Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science 15(1), 37–92 (2005)
Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76, 95–120 (1988)
Cousineau, D.: Un plongement conservatif des Pure Type Systems dans le lambda Pi modulo, Master Parisien de Recherche en Informatique (2006)
Dougherty, D., Ghilezan, S., Lescanne, P., Likavec, S.: Strong normalization of the dual classical sequent calculus, LPAR-2005 (2005)
Dowek, G., Hardin, Th., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31, 33–72 (2003)
Dowek, G., Hardin, Th., Kirchner, C.: HOL-lambda-sigma: an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science 11, 1–25 (2001)
Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic 68(4), 1289–1316 (2003)
Girard, J.Y.: Interprétation Fonctionnelle et Élimination des Coupures dans l’Arithmétique d’Ordre Supérieur, Thèse de Doctorat, Université Paris VII (1972)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993)
Martin-Löf, P.: Intuitionistic Type Theory, Bibliopolis (1984)
Nordström, B., Petersson, K., Smith, J.M.: Martin-Löf’s type theory. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, pp. 1–37. Clarendon Press, Oxford (2000)
Palmgren, E.: On universes in type theory. In: Twenty five years of constructive type theory. Oxford Logic Guides, vol. 36, pp. 191–204. Oxford University Press, New York (1998)
Terlouw, J.: Een nadere bewijstheoretische analyse van GSTT’s, manuscript (1989)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Cousineau, D., Dowek, G. (2007). Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)