The CakeML project has matured since 2012, and is now a practical language with an optimising, end-to-end verified compiler. We turn our attention to performance and usability, aiming to enable useful applications in CakeML which maintain the guarantees of the verified framework.

We are currently investigating a logical relation which will give CakeML a semantic type system, following the approach of projects such as RustBelt. This has several applications, including improved performance in imperative compiler benchmarks, and stronger reasoning about CakeML types.

We first apply the technique to a version of System F with CakeML-like semantics, augmented by existential, general isorecursive, sum, and product types. As in the rest of the CakeML project, our work is formalised in HOL4.