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.
Type de document :
Communication dans un congrès
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. 〈10.1007/978-3-642-15205-4_40〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00497404
Contributeur : Pierre-Yves Strub <>
Soumis le : lundi 5 juillet 2010 - 04:55:04
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 7 octobre 2010 - 11:51:24

Fichier

csl-2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. 〈10.1007/978-3-642-15205-4_40〉. 〈inria-00497404〉

Partager

Métriques

Consultations de la notice

348

Téléchargements de fichiers

339