A Verified Type System for CakeML

CakeML is a dialect of the (strongly typed) ML family of programming

languages, designed to play a central role in high-assurance

software systems. To date, the main artefact supporting this is a verified

compiler from CakeML source code to x86-64 machine code.

The verification effort addresses each phase of compilation from

parsing through to code generation and garbage collection.

In this paper, we focus on the type system: its declarative speci-

fication, type soundness theorem, and the soundness and completeness

of an implementation of type inference – all formally veri-

fied in the HOL4 proof assistant. Each of these aspects of a type

system is important in any design and implementation of a typed

functional programming language. They allow the programmer to

soundly employ (informal) type-based reasoning, and the compiler

to apply optimisations that assume type-correctness. So naturally,

their verification is a critical part of a verified compiler.