Coq Modulo Theory

Pierre-Yves Strub 1
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, INRIA Paris-Rocquencourt
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.
Document type :
Conference papers
Anuj Dawar and Helmut Veith. 19th EACSL Annual Conference on Computer Science Logic, Aug 2010, Brno, Czech Republic. Springer, 6247, pp.529--543, 2010, Lecture Notes in Computer Science; Computer Science Logic, CSL 2010, 19th Annual Conference of the EACSL. <10.1007/978-3-642-15205-4_40>


https://hal.inria.fr/inria-00497404
Contributor : Pierre-Yves Strub <>
Submitted on : Monday, July 5, 2010 - 4:55:04 AM
Last modification on : Wednesday, January 26, 2011 - 11:35:09 AM

File

csl-2010.pdf
fileSource_public_author

Identifiers

Collections

Citation

Pierre-Yves Strub. Coq Modulo Theory. Anuj Dawar and Helmut Veith. 19th EACSL Annual Conference on Computer Science Logic, Aug 2010, Brno, Czech Republic. Springer, 6247, pp.529--543, 2010, Lecture Notes in Computer Science; Computer Science Logic, CSL 2010, 19th Annual Conference of the EACSL. <10.1007/978-3-642-15205-4_40>. <inria-00497404>

Export

Share

Metrics

Consultation de
la notice

232

Téléchargement du document

142