Coq Modulo Theory. Coq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user-defined first-order equational theories. Such a mechanism strictly enriches the system (more terms are typable), eases the use of dependent types and provides more automation during the development of proofs. CoqMT improves over the Calculus of Congruent Inductive Constructions by getting rid of various restrictions and simplifying the type-checking algorithm and the integration of first-order decision procedures. We present here CoqMT, and outline its meta-theoretical study. We also give a brief description of our CoqMT implementation.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
- Jouannaud, Jean-Pierre; Strub, Pierre-Yves: Coq without type casts: a complete proof of Coq Modulo Theory (2017)
- Liu, Jiaxiang; Jouannaud, Jean-Pierre: Confluence: the unifying, expressive power of locality (2014)
- Wang, Qian; Barras, Bruno: Semantics of intensional type theory extended with decidable equational theories (2013)
- Cohen, Cyril; Mahboubi, Assia: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination (2012)
- Strub, Pierre-Yves: Coq Modulo Theory (2010)