Semantics of Intensional Type Theory extended with Decidable Equational Theories

Authors Qian Wang, Bruno Barras

Thumbnail PDF


  • Filesize: 0.48 MB
  • 15 pages

Document Identifiers

Author Details

Qian Wang
Bruno Barras

Cite AsGet BibTex

Qian Wang and Bruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 653-667, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


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 undecidable 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 formalism. 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.
  • Calculus of Constructions
  • Extensional Type Theory
  • Intensional Type Theory
  • Model
  • Meta-theory
  • Consistency
  • Strong Normalization
  • Presburger Arithme


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads