Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk)

on YouTube ↗12m

" summary

Brack is a verified compiler for Scheme implemented in HOL4 that compiles a small subset (lambdas, lists, mutation) to ML and leans on CakeML to get down to machine code, composing semantic-preservation proofs to produce a complete verified toolchain. It uses a CPS transform derived by refunctionalization from a small-step CSK-style semantics, handles first-class continuations (call/cc), and delivers a single-pass compiler whose correctness is simulation-proven and integrated with CakeML’s back end.

AI-written summary · about

" chapters (11)

1. 0:00Brack compiler intro
2. 0:23What Brack is
3. 1:05Verified compilation
4. 2:09Proof structure
5. 2:51Scheme subset
6. 3:35CPS transform
7. 4:57Refunctionalization example
8. 6:40Scheme to ML via CPS
9. 8:45Call/cc handling
10. 9:27Brack benefits
11. 9:48Q&A