Skip to main content

A New Verified Compiler Backend for CakeML

Tan, Yong Kiam, Myreen, Magnus O., Kumar, Ramana, Fooks, Anthony R., Owens, Scott, Norrish, Michael (2016) A New Verified Compiler Backend for CakeML. In: ICFP'16: ACM SIGPLAN International Conference on Functional Programming. . pp. 60-73. Association for Computing Machinery, New York United States ISBN 978-1-4503-4219-3. (doi:10.1145/2951913.2951924) (KAR id:55687)

PDF Author's Accepted Manuscript
Language: English
Download (317kB) Preview
[img]
Preview
Official URL
https://doi.org/10.1145/2951913.2951924

Abstract

We have developed and mechanically verified a new compiler backend for CakeML. Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail. In this way, it resembles mainstream (unverified) compilers for strict functional languages. The compiler supports efficient curried multi-argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more. The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V.

In this paper, we present the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together. We focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations. The entire development has been carried out within the HOL4 theorem prover

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1145/2951913.2951924
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 24 May 2016 17:51 UTC
Last Modified: 24 Jan 2020 12:34 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/55687 (The current URI for this page, for reference purposes)
Owens, Scott: https://orcid.org/0000-0002-7437-4780
  • Depositors only (login required):

Downloads

Downloads per month over past year