Baking for Dafny: A CakeML Backend for Dafny
summary
A verified pipeline translates Dafny IR to CakeML by exporting the IR as S‑expressions, parsing and compiling inside HOL4, and extracting runnable CakeML code; returns and breaks are modeled with exceptions-as-control-flow and loops become tail‑recursive functions. A functional big‑step semantics is formalized in HOL4 and correctness is proved for basic logical and binary operations; datatype support, polymorphic initialisation, and classes/traits remain unimplemented, so the backend runs simple examples but is not yet feature-complete.
AI-written summary · about
chapters (9)
- 0:00Baking for Dafny intro
- 1:29What is CakeML
- 3:14Compiler design overview
- 4:37Dafny to CakeML translation
- 5:59Variables and loops handling
- 7:44Translation correctness proof
- 9:10Current limitations
- 10:34Long-term goals
- 11:35Closing & Q&A
related talks
21mVerified VCG and Verified Compiler for Dafny
24mCakes That Bake Cakes: Dynamic Computation in CakeML
17mPureCake: A Verified Compiler for a Lazy Functional Language
43mFrom CakeML to Proof Checking, and Back Again
15mThey're the same picture: a software-verification flow adapted for hardware verification
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
03mAttempts to design hardware using dafny
15mDo You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs