The CakeML project has built an ecosystem of proofs and tools around an ML dialect called CakeML. The ecosystem includes a proven-correct compiler that can bootstrap itself.

In this talk, I will first give an overview of the entire ecosystem before zooming in on one aspect of the ecosystem, namely, one (of two) compiler frontends for the CakeML compiler.

The frontend in question is an automatic proof-producing tool which given functions in the logic of the HOL4 theorem prover generates CakeML code that is guaranteed to compute the same result as the given HOL functions. This frontend plays a vital role in the in-logic bootstrapping of the CakeML compiler. The tool has recently been extended to be able to generate imperative CakeML code that performs I/O and uses local state.

For more: https://cakeml.org/

I did a B.A. in Computer Science at the University of Oxford, tutored by Dr Jeff Sanders.

I completed my Ph.D. on program verification in 2009 at the University of Cambridge, supervised by Prof. Mike Gordon. My PhD dissertation was selected as the winner of the BCS Distinguished Dissertation Competition 2010.

In 2012, I became a Royal Society Research Fellow, UK.

In 2014, I moved to Chalmers where I became a tenured Associate Professor in 2015.