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

Enrico Tassi (1)

1 MARELLE - Mathematical, Reasoning and Software

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.

Mots clés: Coq; λProlog; metaprogramming; extension language

Domaines: Logique en informatique [cs.LO]; Logiciel mathématique [cs.MS]

Enrico Tassi. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect). The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles (CA), United States. ⟨hal-01637063⟩