Coq without Type Casts: A Complete Proof of Coq Modulo Theory
| Autor: | Jean-Pierre Jouannaud, Pierre-Yves Strub |
|---|---|
| Přispěvatelé: | Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: | |
| Zdroj: | LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana LPAR |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|