2026-07-20T15:08:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4224 2024-03-06T10:34:55Z ddc:004 open_access

Semantics of Intensional Type Theory extended with Decidable Equational Theories Wang, Qian Barras, Bruno Calculus of Constructions Extensional Type Theory Intensional Type Theory Model Meta-theory Consistency Strong Normalization Presburger Arithme 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Qian Wang and Bruno Barras 2013 Is Part Of LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2013.653 urn:nbn:de:0030-drops-42241 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.653 eng https://creativecommons.org/licenses/by/3.0/legalcode