Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Vania Joloboff <>
Submitted on : Tuesday, January 28, 2014 - 7:24:33 AM
Last modification on : Tuesday, March 17, 2020 - 1:54:31 AM




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⟩



Record views