Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Models and termination of proof reduction in the λΠ-calculus modulo theory

Gilles Dowek 1, 2
Abstract : We define a notion of model for the λΠ-calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction terminates in the λΠ-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions .
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01101834
Contributor : Gilles Dowek <>
Submitted on : Wednesday, April 26, 2017 - 7:29:39 PM
Last modification on : Tuesday, July 7, 2020 - 11:52:47 AM
Long-term archiving on: : Thursday, July 27, 2017 - 2:51:28 PM

Files

superpi.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License

Identifiers

  • HAL Id : hal-01101834, version 2
  • ARXIV : 1501.06522

Citation

Gilles Dowek. Models and termination of proof reduction in the λΠ-calculus modulo theory. 2017. ⟨hal-01101834v2⟩

Share

Metrics

Record views

206

Files downloads

170