Trustworthy Systems

A verified type system for CakeML

Authors

Yong Kiam Tan, Scott Owens and Ramana Kumar

ASTAR

University of Kent

Data61
CSIRO

University of Cambridge

Winner: 2016 Peter Landin Prize for best paper

Abstract

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 specification, type soundness theorem, and the soundness and completeness of an implementation of type inference -- all formally verified 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.

BibTeX Entry

  @inproceedings{Tan_OK_16,
    address          = {Koblenz, Germany},
    author           = {Tan, Yong Kiam and Owens, Scott and Kumar, Ramana},
    booktitle        = {Implementation and application of functional and programming languages},
    doi              = {10.1145/2897336.2897344},
    keywords         = {cakeml},
    month            = jul,
    pages            = {12},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8976.pdf},
    title            = {A Verified Type System for {CakeML}},
    year             = {2016}
  }

Download