Coq without Type Casts: A Complete Proof of Coq Modulo Theory

Abstract : Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus. We justify here CoqMT's type-checking algorithm by showing strong normalization as well as the Church-Rosser property of β-reductions augmented with CoqMT's weak and strong T-elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.
Type de document :
Communication dans un congrès
LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana
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-01664457
Contributeur : Pierre-Yves Strub <>
Soumis le : jeudi 14 décembre 2017 - 19:00:55
Dernière modification le : jeudi 10 mai 2018 - 02:06:49

Fichier

final-version.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01664457, version 1

Citation

Jean-Pierre Jouannaud, Pierre-Yves Strub. Coq without Type Casts: A Complete Proof of Coq Modulo Theory. LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana. 〈hal-01664457〉

Partager

Métriques

Consultations de la notice

224

Téléchargements de fichiers

50