Paper Info
Title
A verified type system for CakeML.
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.
Year
DOI
Venue
2015
10.1145/2897336.2897344
IFL
Field
DocType
Citations 
Type system,Programming language,Functional compiler,Computer science,Compiler correctness,Theoretical computer science,Code generation,Type inference,Compiler,Data type,Compiler construction
Conference
2
PageRank 
References 
Authors
0.40
9
3
Name
Order
Citations
PageRank
Yong Kiam Tan110712.93
Scott Owens2232.65
Ramana Kumar314113.56