The CakeML Project: Verified Compilation, Verified Bootstrapping, Just-In-Time Compilation, and Applications

This talk will be about the CakeML project. The CakeML project centres around an impure functional programming language, for which we have developed a collection of proofs and tools inside the HOL4 theorem prover. The development includes a proven-correct compiler that can bootstrap itself.

This talk has two parts.

In the first part, I will explain the research questions the CakeML project has tackled and outline the main research ideas that have helped us address them. The research questions include:

• how can we transfer properties proved of logic functions to properties of machine code compiled from those functions?
• how can we use a verified compiler to compile itself?
• how can we reason about space usage of CakeML programs?
• how can we prove liveness properties for non-terminating code?

• built a proved-to-be-sound clone of the HOL light theorem prover
• produced a verified compiler for a Haskell-like language
• constructed several verified checkers, including checkers for UNSAT proofs, floating-point error bounds, OpenTheory article files, pseudo- Boolean proofs, and Integer Programming proofs