Paper Info
Title
The verified CakeML compiler backend.
Abstract
The CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are compiled away incrementally, enables verification of each compilation pass at an appropriate level of semantic detail. Parts of the compiler's implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multiargument functions, configurable data representations, efficient exceptions, register allocation, and more. The compiler produces machine code for five architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generated machine code contains the verified runtime system which includes a verified generational copying garbage collector and a verified arbitrary precision arithmetic (bignum) library. In this paper, we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs fit together and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.
Year
DOI
Venue
2019
10.1017/S0956796818000229
JOURNAL OF FUNCTIONAL PROGRAMMING
Field
DocType
Volume
Programming language,Register allocation,Functional programming,Computer science,Automated theorem proving,Compiler,Machine code,Garbage collection,Computer programming,Runtime system
Journal
29
ISSN
Citations 
PageRank 
0956-7968
2
0.38
References 
Authors
26
6
Name
Order
Citations
PageRank
Yong Kiam Tan110712.93
Magnus O. Myreen262135.67
Ramana Kumar314113.56
Anthony C. J. Fox417510.70
Scott Owens568326.50
Michael Norrish6109161.77