Skip to main content
Kent Academic Repository

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) (KAR id:53891)

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 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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 31 Jan 2016 20:22 UTC
Last Modified: 09 Dec 2022 00:24 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/53891 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.