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.
Type de document :
Pré-publication, Document de travail
2018
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01637063
Contributeur : Enrico Tassi <>
Soumis le : vendredi 17 novembre 2017 - 11:44:42
Dernière modification le : mardi 17 avril 2018 - 09:04:41
Document(s) archivé(s) le : dimanche 18 février 2018 - 13:46:57

Fichier

coqpl2018.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

180

Téléchargements de fichiers

109