Title: Elpi: rule-based extension language
Abstract:
This document presents Elpi, a rule-based language designed to extend applications such as
interactive theorem provers, notably Rocq. Elpi combines λProlog, a higher-order logic pro-
gramming language, with Constraint Handling Rules, enabling concise and expressive manip-
ulation of syntax trees that include binders and holes.
The manuscript presents Elpi as a programming language and contrasts it with Prolog and
λProlog. It then describes the implementation, highlighting the factors that contribute to its
efficiency and the ease with which it can be integrated into host applications. The text continues
with details on Elpi’s integration with Rocq and concludes with a survey of applications built
on Elpi, identifying the language features most relevant to each.
Two case studies illustrate Elpi’s capabilities. The first presents a version of the Hindley-Milner
type inference algorithm. The second describes a proof-transfer tool for Rocq.
File: pdf
Related software: elpi rocq-elpi
Date: January 9, 2026
Place: Inria - 2004 Rte des Lucioles, 06560 Valbonne, France
Time: 2PM
Room: Coriolis (bat. Galois)
Video stream: https://inria.webex.com/inria/j.php?MTID=m9fea78e0ac3aee1d89bfaba57c337890
Slides: pdf html