The Coq mailing list

[Enrico Tassi <Enrico.Tassi AT inria.fr>]

Dear Coq-Club,

   I'm proud to announce that the Elpi extension language for Coq 8.10
is available to download.

Elpi is a dialect of λProlog, a programming language well suited to
manipulate abstract syntax trees containing binders and unification
variables.

Coq-Elpi wraps Elpi in a Coq plugin and provides a representation of
Coq's terms based on Higher-Order Abstract Syntax.
It also exports to Elpi a comprehensive set of Coq's primitives, so
that one can access the environment of theorems and data types, define
new constants, declare implicit arguments, type classes instances, ...
and finally implement commands and tactics.

Some programs written in Coq-Elpi worth mentioning are:
- binary and unary parametricity translation (by Cyril Cohen)
- derivation of strong induction principles for nested data types
- derivation of proved equality tests on inductive data

If you are curious you can find installation instructions, a couple of
tutorials and a few more examples at the following address:
  https://github.com/LPCIC/coq-elpi

Any feedback is very welcome.

Best regards,
-- 
Enrico Tassi