LFCS seminar : Magnus Myreen: CakeML: a formally verified implementation of ML

Abstract:

I will present the CakeML project. This project centres around a
subset of ML that is carefully chosen to be easy to write programs
in and convenient to reason about formally. I will talk about
results so far, in particular, our a formally verified
implementation of CakeML (a compiler and a read-eval-print loop) in
64-bit x86 machine code. The construction and verification of this
implementation required both proofs of high-level programs (the
parser, type inferencer and compiler) and low-level programs (the
runtime in x86 machine code, its bignum library and garbage
collector). We used a novel technique to produce much of the
verified low-level code: we bootstrapped the verified compiler
algorithm, within higher-order logic, to produce the verified
low-level implementation. We proved divergence preservation using
simple clocks. This work was carried out using the HOL4 theorem
prover and is a collaborative effort, where the main contributors
are Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens.