Kanren Light
summary
An experimental system implemented on top of HOL Light tactics brings miniKanren-style relational programming inside a theorem prover and synthesizes candidate substitutions together with theorem certificates checked by HOL Light. Core components are solvers as OCaml procedures with combinators (then, repeat, interleave) plus explicit meta-variables and backtracking. Examples include an append relation and a small Lisp evaluator that succeeds and even enumerates quines. Search completeness is not guaranteed so proofs are dynamically semi-certified; future work targets higher-order unification and CLP.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:21Relational Programming
- 3:07Core Objects
- 6:30Example
- 10:32Terminology
- 11:43refinement by tactics
- 12:48refinement by solvers
- 13:43solver tactics
- 14:20interactivity
- 16:42steplv
- 18:10quark
- 19:28Conclusion
related talks
40mminiKanren Philosophy
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
16mMulti-stage Relational Programming
47mLogic Programming à la Carte
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
24mAll for one and none forall: Compiling polymorphic relations without(…)
23mTyped Embedding of miniKanren for Functional Conversion