Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo

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. The λΠ-calculus is a dependently typed lambda-calculus that allows to express proofs of minimal predicate logic through the Brouwer-Heyting-Kolmogorov interpretation and the Curry-de Bruijn-Howard correspondence. It can be extended in several ways to express proofs of some theory. A first solution is to express the theory in Deduction modulo [7, 9], i.e. to orient the axioms as rewrite rules and to extend the λΠ-calculus to express proofs in Deduction modulo [3]. We get this way the λΠ-calculus modulo...

• Type: Conference
• Year: 2007
• Where: TLCA
• Authors: Denis Cousineau 0002, Gilles Dowek
• Keywords: Deduction Modulo, Minimal Predicate Logic, Pure Type Systems, Theoretical Computer Science, TLCA 2007