Coq Modulo Theory - Short Paper

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.
Document type :
Conference papers
Logic In Computer Science (LICS 2010), Jul 2010, Edimbourg, United Kingdom


https://hal.inria.fr/inria-00497794
Contributor : Pierre-Yves Strub <>
Submitted on : Monday, July 5, 2010 - 11:51:58 PM
Last modification on : Tuesday, July 6, 2010 - 9:37:34 AM

File

lics-2010.pdf
fileSource_public_author

Identifiers

  • HAL Id : inria-00497794, version 1

Collections

Citation

Pierre-Yves Strub, Qian Wang. Coq Modulo Theory - Short Paper. Logic In Computer Science (LICS 2010), Jul 2010, Edimbourg, United Kingdom. <inria-00497794>

Export

Share

Metrics

Consultation de
la notice

187

Téléchargement du document

48