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.

Neng-Fa Zhou, Canonicalizing High-Level Constructs in Picat, PADL 2017. Picat replaces a function call f(t1,...,tn) by a new variable V and inserts a predicate call p(t1,...,tn,V) before the enclosing goal, independently arriving at close to the same transformation as spilling, for the same reason: recovering functional syntax over a logic-programming core.

Sergio Antoy, Michael Hanus, Andy Jost and Steven Libby, ICurry, Declare 2019. Curry’s intermediate representation, FlatCurry, normalizes nested function calls the same way via let-insertion; cited from Spilling and functional syntax as a relative of the same transformation.

Amr Sabry and Matthias Felleisen, Reasoning about Programs in Continuation-Passing Style, LFP 1992. With Flanagan, Sabry, Duba & Felleisen, PLDI 1993, introduces A-normal form, the functional-compiler ancestor of spilling: both flatten nested expressions by let-binding every intermediate result, where Elpi’s pi/sigma play the role let/lambda play in ANF.

Cormac Flanagan, Amr Sabry, Bruce F. Duba and Matthias Felleisen, The Essence of Compiling with Continuations, PLDI 1993. See Sabry & Felleisen, LFP 1992, cited alongside it from Spilling and functional syntax.

Markus Triska, The Finite Domain Constraint Solver of SWI-Prolog, FLOPS 2012. Prolog’s CLP(FD) flattens arithmetic expressions the same way spilling does, scoped to arithmetic: X #= Y+Z*W compiles to a sequence of primitive constraint goals over fresh variables via goal_expansion/2.