Adventures in extending miniKanren
summary
Adds a stage miniKanren interpreter that turns interpreters into compilers and an SMT-backed CLP SMT extension by augmenting the miniKanren state with extra fields; implements both in the faster miniKanren codebase and demo repos. Key results: a Prolog-like baseline synthesis run takes ~8s, the staged pipeline generates code in ~0.05s and completes synthesis in ~0.5s, while the direct CLP(SMT) version spends ~32s due to frequent solver calls. The extensions work and the state-extension pattern is small and mechanical.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:15Agenda
- 0:57Syntax
- 13:19Stage interpreter
- 15:35Stage interpreter example
- 17:52Stage relation interpreter
- 22:57Closures interpreter
- 24:07Benchmarks
- 26:51clp smt
- 33:59fastminicameron
- 37:08stageminicameron
- 41:06outro
related talks
16mMulti-stage Relational Programming
20mKanren Light
19mSome Novel miniKanren Synthesis Tasks
15mAn Empirical Study of Partial Deduction for miniKanren
40mminiKanren Philosophy
23mTyped Embedding of miniKanren for Functional Conversion
40mμKanren: Running the Little Things Backwards
22mA Case Study in Functional Conversion and Mode Inference in miniKanren