I study programming languages and formal verification via interactive theorem-proving: I consider mathematically rigorous specifications of programming languages, and try to prove interesting properties about them using machine-assisted reasoning.

My focus is CakeML: an open-source, ML-like programming language, verified compiler, and proof ecosystem. The CakeML language, semantics, and compiler algorithm are all specified in higher-order logic (HOL), using the interactive theorem-prover HOL4. This allows both end-to-end verification of the compiler, and bootstrapping within the logic.


My project

My project is titled “Building Verified Applications in CakeML” and is funded by the UK Research Institute in Verified Trustworthy Software Systems (VeTSS).

I gave a talk on my current work in Dec 2020 - contact me if you would like to see a recording.

As the CakeML project matures, I aim to create practical techniques for writing useful, verified applications in CakeML. I am particularly interested in improving performance in imperative compiler benchmarks, without compromising the guarantees provided by the CakeML ecosystem – currently, we suffer as we cannot straightforwardly use array accesses which are not bounds-checked. This is due to the formulation of our compiler correctness result.

Compiler correctness in CakeML

The CakeML compiler is proved to preserve the semantics of input source programs in output machine code, according to validated models of instruction set architectures. However, our compiler correctness result requires the input source program to be well-formed - it must have a well-defined semantics (i.e. it does not get stuck, or cause a runtime type error).

Currently, this condition is enforced in one of three ways:

However, each of these has its own limitations:

We would like a trade-off between these methods, so that we can combine the compositionality and ease-of-use of syntactic typing or translation from HOL, with the expressivity of proof in separation logic - but while avoiding the restrictions of the former and the effort of the latter. We believe semantic type soundness holds the key.

Semantic type soundness for CakeML

My current aim is to produce a semantic type soundness result for CakeML. This would permit reasoning about programs that are safe to use as if they have a certain type, but are not syntactically typeable.

Semantic type soundness is well-studied (see here for a presentation), and requires construction of a unary, step-indexed logical relation which expresses “semantic typing”. Any notion of semantic typing must be proved compatible with syntactic typing: for every syntactic typing rule, we should be able to derive a semantic equivalent. However, expressing a suitable logical relation in the simply-typed logic of HOL4 is not at all straightforward.

Ideally, our notion of semantic typing could integrate with the existing CakeML proof ecosystem in some way (in particular, with refinement invariants and characteristic formulae). This would permit the re-use of existing proofs in these frameworks to derive semantic typing results.

Uses in CakeML

Other work

Translation from higher-order logic to stateful CakeML

This work has been published.

I worked with Oskar Abrahamsson and other developers to improve CakeML’s monadic translator. This machinery augments CakeML’s pure translator, translating HOL functions written in a state-and-exception monad to stateful CakeML.

In particular, I contributed the following: