Semantics of Intensional Type Theory extended with Decidable Equational Theories

Qian Wang 1 Bruno Barras 2
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
2 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Type de document :
Communication dans un congrès
Simona Ronchi Della Rocca. Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 23, pp.653--667, 2013, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CSL.2013.653〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00937197
Contributeur : Vania Joloboff <>
Soumis le : mardi 28 janvier 2014 - 07:24:33
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

Collections

Citation

Qian Wang, Bruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories. Simona Ronchi Della Rocca. Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 23, pp.653--667, 2013, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CSL.2013.653〉. 〈hal-00937197〉

Partager

Métriques

Consultations de la notice

209