Semantics of Intensional Type Theory extended with Decidable Equational Theories - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

Semantics of Intensional Type Theory extended with Decidable Equational Theories

(1) , (2)
1
2

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.
Not file

Dates and versions

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

Identifiers

Cite

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⟩
157 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More