Skip to main content

A Verified Type System for CakeML

Tan, Yong Kiam, Owens, Scott, Kumar, Ramana (2015) A Verified Type System for CakeML. In: Implementation and application of functional programming languages, 14-16 September, 2015, Koblenz, Germany. (doi:10.1145/2897336.2897344)

PDF - Author's Accepted Manuscript
Download (268kB) Preview
Official URL


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.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1145/2897336.2897344
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 31 Jan 2016 20:22 UTC
Last Modified: 29 May 2019 16:55 UTC
Resource URI: (The current URI for this page, for reference purposes)
Owens, Scott:
  • Depositors only (login required):


Downloads per month over past year