ELAN for equational reasoning in Coq

Quang-Huy Nguyen 1 Cuihtlauac Alvarado
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We describe an interface between \textsf{Coq}, an interactive theorem-prover based on type theory and \textsf{ELAN}, an automated deduction system based on rewriting logic. Our objective is to provide efficient tools to implement decision procedures using equational reasoning in \textsf{Coq}. \textsf{ELAN} is used as a rewrite engine. Reflection is used in \textsf{Coq} to translate back the delegated rewrite computations. A rewriting trace is returned from \textsf{ELAN} and replayed in \textsf{Coq}. Correctness is ensured by this replaying which builds a complete proof-term.
Type de document :
Communication dans un congrès
INRIA. 2nd Workshop on Logical Frameworks & Metalanguage - LFM'00, Jun 2000, Santa Barbara, USA, 14 p, 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00107864
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:12:09
Dernière modification le : samedi 26 mai 2018 - 01:17:52
Document(s) archivé(s) le : mercredi 29 mars 2017 - 13:11:22

Identifiants

  • HAL Id : inria-00107864, version 1

Citation

Quang-Huy Nguyen, Cuihtlauac Alvarado. ELAN for equational reasoning in Coq. INRIA. 2nd Workshop on Logical Frameworks & Metalanguage - LFM'00, Jun 2000, Santa Barbara, USA, 14 p, 2000. 〈inria-00107864〉

Partager

Métriques

Consultations de la notice

171

Téléchargements de fichiers

70