Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect) - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

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

(1)
1
Enrico Tassi

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.
Fichier principal
Vignette du fichier
coqpl2018.pdf (527.9 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01637063 , version 1 (17-11-2017)

Identifiers

  • HAL Id : hal-01637063 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More