Sciweavers

Share
TLCA
2007
Springer

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

9 years 17 days ago
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...
Denis Cousineau 0002, Gilles Dowek
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TLCA
Authors Denis Cousineau 0002, Gilles Dowek
Comments (0)
books