Cakes That Bake Cakes: Dynamic Computation in CakeML
summary
Extends the verified CakeML compiler with an Eval primitive that compiles and executes new CakeML code at runtime, letting original and dynamic code share higher‑order values and mutually recurse and enabling a verified LCF‑style prover like Candle to run tactics down to the binary. Implementation modifies the self‑hosting pipeline, requires x86 Linux, updates about 50,000 lines of proofs inside a ~320,000 lines of HOL4 development, and proves correctness using an oracle-based semantics to reconcile compilation phases.
AI-written summary · about
chapters (10)
- 0:00Dynamic computation in CakeML
- 3:10Meaning of eval in CakeML
- 5:39Motivation for eval
- 7:04Eval compiler implementation
- 11:41CakeML compiler structure
- 13:26Runtime state and eval design
- 15:32Namespaces and environments
- 17:18Eval challenges and proofs
- 19:42Eval verification summary
- 20:25Q&A
related talks
43mFrom CakeML to Proof Checking, and Back Again
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
15mThey're the same picture: a software-verification flow adapted for hardware verification
18mBaking for Dafny: A CakeML Backend for Dafny
15mDo You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
21mVerified VCG and Verified Compiler for Dafny
41mConcatenative programming and stack-based languages
24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...