Programming languages

The design, specification and implementation of programming languages is essential for building trustworthy systems. Programs expressed in well-designed languages are easier to specify, verify, optimise, and maintain.

Cogent

Cogent combines the ease of verification of functional languages with innovative facilities for low-level systems programming.

CakeML

CakeML is a landmark implementation of a fully verified compiler for a high-level functional language.

MicroVM

The Micro Virtual Machine project aims to simplify language implementations, by providing a virtual machine layer that is efficient, reusable and amenable to formal verification.

L4.verified C semantics

We have developed a detailed formalisation of a large subset of the C language. This is implemented in our C parser and is used for our verification of seL4.