Coq Modulo Theory - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2010

Coq Modulo Theory

Pierre-Yves Strub
  • Function : Author
  • PersonId : 857170

Abstract

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.
Fichier principal
Vignette du fichier
csl-2010.pdf (158.1 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00497404 , version 1 (05-07-2010)

Identifiers

Cite

Pierre-Yves Strub. Coq Modulo Theory. 19th EACSL Annual Conference on Computer Science Logic, Aug 2010, Brno, Czech Republic. pp.529--543, ⟨10.1007/978-3-642-15205-4_40⟩. ⟨inria-00497404⟩
222 View
442 Download

Altmetric

Share

Gmail Facebook X LinkedIn More