Models and termination of proof-reduction in the $\lambda$$\Pi$-calculus modulo theory

Research paper by Gilles Dowek

Indexed on: 26 Jan '15Published on: 26 Jan '15Published in: Computer Science - Logic in Computer Science


We define a notion of model for the $\lambda \Pi$-calculus modulo theory, a notion of super-consistent theory, and prove that proof-reduction terminates in the $\lambda \Pi$-calculus modulo a super-consistent theory. We prove this way the termination of proof-reduction in two theories in the $\lambda \Pi$-calculus modulo theory, and their consistency: an embedding of Simple type theory and an embedding of the Calculus of constructions.