λKanren: Higher-order Logic Programming with Shallow Embedding
summary
λKanren is a shallow‑embedding of a subset of higher‑order hereditary Harrop formulas built by adding about 40 lines to the TRS2 chapter 10 miniKanren core (excluding the separate higher‑order unification module). It exposes new operators assume and all, supports binding constructors tie and app, and implements unification up to alpha and beta equivalence; examples include proving append properties, scoped existential/nominal behavior, and synthesizing the identity as the only valid higher‑order witness.
AI-written summary · about
chapters (6)
related talks
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
40mminiKanren Philosophy
16mMulti-stage Relational Programming
23mTyped Embedding of miniKanren for Functional Conversion
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
24mAll for one and none forall: Compiling polymorphic relations without(…)
40mμKanren: Running the Little Things Backwards
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving