A Verified Type System for CakeML

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

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


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)
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: 08 May 2018 09:01 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/53891 (The current URI for this page, for reference purposes)
Owens, Scott: https://orcid.org/0000-0002-7437-4780
  • Depositors only (login required):


Downloads per month over past year