Thursday 18 June 2020, 14:00, online: Elpi, the extension language for your ITP, Enrico Tassi (marelle, Inria Sophia antipolis).
Elpi[1] is an interpreter for a dialect of lambdaProlog that can be embedded in OCaml applications as an extension language. As in plain lambdaProlog it lets one represent syntax trees with binders using HOAS, providing binding and substitution as language primitives. In addition to that it provides modes, constraints and constraint handling rules to let one use the unification variables of lambdaProlog to represent "holes" in the syntax trees (sometimes called meta variables, or goals, in ITPs). As a result the runtime is take care of bookkeeping the meta variable assignment; Higher Order (pattern) unification takes care of meta variable scope and occur check at assignment time; constraints represent properties of holes (such as having a type) and are automatically resumed in order to checked that property when a term is used to fill a hole.
Elpi can today be used to implement new commands and tactics for the Coq system. It was used to derive proved equality tests from inductive type declarations[2], and to elaborate the Hierarchy Builder language down to the jungle of records, coercions, unification hints, notations, implicit arguments, sections and modules that constitute the "packed classes" discipline for algebraic hierarchies adopted by the Mathematical Components library[3].
It is ongoing work to link Foundational Proof Certificates with Coq[4] and to implement a new elaborator for Coq (featuring unification hints, type classes, coercions, etc...) in the spirit of [5].
In this talk I'll introduce Elpi as a programming language and give a demo of the integration of Elpi in Coq. Time permitting I'll show some OCaml API and example code constituting the glue between Elpi and a host system.