PureCake: A Verified Compiler for a Lazy Functional Language
summary
PureCake is a mechanically verified compiler built in HOL4 that translates a Haskell-like lazy language, PureLang, down to machine code by targeting and composing with CakeML’s verified compiler, claiming the first end-to-end proof for a lazy language. It verifies two-phase constraint-based Hindley–Milner inference, demand analysis to eliminate thunk allocation, and a back end with thunk-to-array sharing; verification covers seven syntactic relations, three intermediate languages, and an end-to-end theorem modulo out-of-memory.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:15Language guarantees
- 0:50Binary level guarantees
- 1:26Verified compilation
- 2:11PureCake
- 2:46PureLang
- 3:06PureLang features
- 3:48Compiler Expressions
- 4:26Operational Semantics
- 6:29Compiler
- 6:45Type Inference
- 7:22Demand Analysis
- 8:53Compiler Backend
- 10:18ThunLang
- 11:15StateLang
- 12:49Endtoend correctness
- 13:38Questions
related talks
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
43mFrom CakeML to Proof Checking, and Back Again
15mThey're the same picture: a software-verification flow adapted for hardware verification
21mVerified VCG and Verified Compiler for Dafny
18mBaking for Dafny: A CakeML Backend for Dafny
24mFormally Verified Native Code Generation in an Effectful JIT: Turning the CompCe...
18mA Verified Compiler for a Functional Tensor Language
15mDo You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs