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 <>
Submitted on : Thursday, October 19, 2006 - 9:12:09 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
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