Semantics of Intensional Type Theory extended with Decidable Equational Theories - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Semantics of Intensional Type Theory extended with Decidable Equational Theories

Résumé

Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions (CC) provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality generally leads to undecid- able type-checking, it seems a reasonable trade-off to extend intensional equality with a decidable first-order theory, as experimented in earlier work on CoqMTU and its implementation CoqMT . In this work, CoqMTU is extended with strong eliminations. The meta-theoretical study, particularly the part relying on semantic arguments, is more complex. A set-theoretical model of the equational theory is the key ingredient to derive the logical consistency of the formal- ism. Strong normalization, the main lemma from which type-decidability follows, is proved by attaching realizability information to the values of the model. The approach we have followed is to first consider an abstract notion of first-order equational theory, and then instantiate it with a particular instance, Presburger Arithmetic. These results have been formalized using Coq.
Fichier non déposé

Dates et versions

hal-00937197 , version 1 (28-01-2014)

Identifiants

Citer

Qian Wang, Bruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories. Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. pp.653--667, ⟨10.4230/LIPIcs.CSL.2013.653⟩. ⟨hal-00937197⟩
163 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More