Full Workshop
summary
Symbolic execution produces a symbolic scheme that exposes schedule, unification and reification costs and shows scheduling dominates some pathologies (sometimes relations run faster backward) and occurs‑checks blow up costs; a prototype formal model is usable but semi‑manual. A staging‑as‑compilation extension turns an interpreter into generated code and cuts a fib synthesis run from ~8s (parliament) to ~0.5s (staged), while a CLP‑SMT hookup works but spends ~32s on arithmetic queries. Guarded fresh defers bindings to share constraints across multiple evalo calls and speeds XOR and recursive list synthesis. Higher‑order unification uses static closures to handle alpha/scope; a minimal relational floating‑point library reveals multiplication time exploding with certain mantissa patterns. Repos live on the faster‑miniKanren / metacannon branches; many parts remain experimental.
AI-written summary · about
chapters (25)
- 0:00Start
- 8:00Introduction Kickoff
- 8:55Keynotes
- 12:16How Do Live Talks Work
- 21:53Analysis of Scheduling Time
- 24:23Analysis of Unification and Verification Time
- 51:44Shallow Relational Interpreter
- 53:28Evaluate Goal Expressions
- 1:08:05External Grounding
- 1:08:21Limitations of the Current Interpreter
- 1:18:56Patent Restriction
- 1:21:13The Unification Algorithm
- 1:29:56Static Closures
- 1:34:25Introductions
- 1:43:35Keynote
- 2:00:15Interpreters into Compilers
- 2:05:40Stage Interpreter
- 2:11:55Benchmarks
- 2:13:12Parsing with Derivatives
- 2:15:44Factorial
- 2:18:51Synthesis
- 2:22:46Implement a Log Extension
- 2:24:57Implementation of Stage Mini Camera
- 2:28:59The Code
- 2:31:01Resource Allocation
related talks
16mCompiling Symbolic Execution with Staging and Algebraic Effects
29mPartially Evaluating Symbolic Interpreters for All
01h 31m"Thoughts on language evolution"
31mLetting users do the undecidable: lessons from program synthesis
16mMulti-stage Relational Programming
14mCollapsing Towers for Side-Channel Security
51mSynthesis and Verification for All
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures