Bibliography

Enrico Tassi, Elpi: rule-based extension language, HDR thesis (9 January 2026). The most complete account of Elpi’s design and its applications; the primary source for this manual’s Semantics part.

Davide Fissore and Enrico Tassi, Determinacy Checking for Elpi: an Higher-Order Logic Programming language with Cut, PADL 2026 (LNCS 16401). The formal treatment behind Determinacy checking.

Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen and Enrico Tassi, ELPI: Fast, Embeddable, λProlog Interpreter, LPAR-20 (2015). The original system description; cite this one for Elpi itself.

Gregory J. Duck, Peter J. Stuckey, María García de la Banda and Christian Holzbaur, The Refined Operational Semantics of Constraint Handling Rules, Logic Programming (ICLP 2004), Springer, pages 90–104. The paper that names and defines the refined operational semantics Elpi implements for CHR, behind The constraint store and Formal semantics.

Jon Sneyers, Peter Van Weert, Tom Schrijvers and Leslie De Koninck, As time goes by: Constraint Handling Rules — A survey of CHR research from 1998 to 2007, Theory and Practice of Logic Programming 10(1), 2010, pages 1–47. A broad survey of CHR as a general-purpose declarative formalism: its semantics, program analysis, implementations, extensions and applications; cited from Introduction for what CHR is.

Ferruccio Guidi, Claudio Sacerdoti Coen and Enrico Tassi, Implementing type theory in higher order constraint logic programming, Mathematical Structures in Computer Science 29(8), 2019. Constraints and constraint handling rules, formally; cited throughout The constraint store and Formal semantics.

Enrico Tassi, Elpi: an extension language with binders and unification variables, slides from the ML Family Workshop 2018. A lightweight, slide-shaped introduction; its companion code, toyml, implements Algorithm W in Elpi and is a second, independent take on Hindley-Milner type inference.

Dale Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Journal of Logic and Computation 1(4), 1991, pages 497–536. Introduces the higher-order pattern fragment (Lλ) that Elpi restricts unification variables to; see Unification and variables.

Dale Miller, Unification under a mixed prefix, Journal of Symbolic Computation 14(4), 1992, pages 321–358. The most-general-extension property behind the unify function of Formal semantics.

Dale Miller and Gopalan Nadathur, Programming with Higher-Order Logic, Cambridge University Press, 2012. The reference for standard λProlog, which this manual assumes throughout rather than re-teaching (Introduction).

Neng-Fa Zhou, The Language Features and Architecture of B-Prolog, Theory and Practice of Logic Programming 12(1–2), 2012, pages 189–218. Introduces B-Prolog’s matching clauses, whose one-way head matching is the idea behind Elpi’s input-mode arguments; see Logic Programming and Constraints.

Spiro Michaylov and Frank Pfenning, Higher-Order Logic Programming as Constraint Logic Programming, Proceedings of the First Workshop on Principles and Practice of Constraint Programming, Brown University, 1993, pages 221–229. Reads a higher-order logic programming language as a constraint logic programming one; the constraint-resume rule of Formal semantics follows it.