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

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 .
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01101834
Contributeur : Gilles Dowek <>
Soumis le : mercredi 26 avril 2017 - 19:29:39
Dernière modification le : mardi 17 avril 2018 - 09:04:14
Document(s) archivé(s) le : jeudi 27 juillet 2017 - 14:51:28

Fichiers

superpi.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Partage selon les Conditions Initiales 4.0 International License

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

175

Téléchargements de fichiers

64