Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
summary
Presents a concrete, verified space-cost semantics for CakeML by formalizing a dataLang cost semantics that measures heap and stack with a size_of function using timestamps to avoid double-counting; it adds runtime checks that set a safe_for_space predicate false when limits are exceeded. Proves soundness w.r.t. the CakeML compiler that uses garbage collection, shows size_of is idempotent under GC, and mechanizes proofs in HOL4 formalization, so compiled code cannot introduce new out-of-memory behaviours.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:32What is CakeML
- 1:38Objectives
- 2:16Why Programs Run Out of Memory
- 3:59KML
- 4:49DataLag
- 5:42Example FullL
- 7:47Example List
- 9:50How it works
- 10:34Example
- 12:07Counting Values
- 12:35Sizeof
- 13:40Counting
- 14:48Conclusion
related talks
24mCakes That Bake Cakes: Dynamic Computation in CakeML
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
18mMulti Types and Reasonable Space
43mFrom CakeML to Proof Checking, and Back Again
17mPureCake: A Verified Compiler for a Lazy Functional Language
18mCutting the Cake: A Language for Fair Division
18mBaking for Dafny: A CakeML Backend for Dafny
41mConcatenative programming and stack-based languages