Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)

Enrico Tassi 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Elpi is dialect of λProlog that can be used as an extension language for Coq. It lets one define commands and tactics in a high level programming language tailored to the manipulation of syntax trees containing binders and existentially quantified meta variables.
Complete list of metadatas

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/hal-01637063
Contributor : Enrico Tassi <>
Submitted on : Friday, November 17, 2017 - 11:44:42 AM
Last modification on : Tuesday, April 17, 2018 - 9:04:41 AM
Long-term archiving on : Sunday, February 18, 2018 - 1:46:57 PM

File

coqpl2018.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01637063, version 1

Collections

Citation

Enrico Tassi. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect). 2018. ⟨hal-01637063⟩

Share

Metrics

Record views

326

Files downloads

254