Cakes That Bake Cakes: Dynamic Computation in CakeML

Explore the groundbreaking extension of the verified CakeML compiler in this 24-minute conference talk from PLDI 2023. Delve into the implementation of a new language primitive, Eval, which enables runtime evaluation of new CakeML syntax. Discover how this ambitious form of compilation at runtime and dynamic execution allows original and dynamically added code to share higher-order values and recursively call each other. Learn about the extensive modifications made to the modern CakeML compiler pipeline and proofs to support dynamic computation semantics. Gain insights into the design decisions, proof techniques, and proof engineering lessons from this project, including unexpected complications encountered along the way. Understand the significance of this implementation as the first verified run-time environment capable of supporting a standard LCF-style theorem prover design.