HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2006 - 9:12:09 AM
Last modification on : Friday, February 4, 2022 - 3:23:16 AM
Long-term archiving on: : Wednesday, March 29, 2017 - 1:11:22 PM


  • HAL Id : inria-00107864, version 1



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



Record views


Files downloads