Embedding Pure Type Systems in the lambda-Pi-calculus modulo
Preprint
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.Keywords
All Related Versions
This publication has 4 references indexed in Scilit:
- Definitions by rewriting in the Calculus of ConstructionsMathematical Structures in Computer Science, 2005
- Strong Normalization of the Dual Classical Sequent CalculusLecture Notes in Computer Science, 2005
- Proof normalization moduloThe Journal of Symbolic Logic, 2003
- Theorem Proving ModuloJournal of Automated Reasoning, 2003