Skip to main content

The verified CakeML compiler backend

Authors

Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish

Carnegie Mellon University

University of Kent

DATA61

DeepMind

Chalmers University of Technology

University of Cambridge

Australian National University

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 com- piler’s implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multi-argument 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.

BibTeX Entry

  @article{Tan_MKFON_19,
    doi              = {https://doi.org/10.1017/S0956796818000229},
    author           = {Tan, Yong Kiam and Myreen, Magnus and Kumar, Ramana and Fox, Anthony and Owens, Scott and Norrish,
                        Michael},
    month            = feb,
    date             = {2019-2-4},
    numpages         = {57},
    title            = {The verified {CakeML} compiler backend},
    year             = {2019},
    volume           = {29},
    journal          = {Journal of Functional Programming},
    publisher        = {Cambridge University Press}
  }

Download

Served by Apache on Linux on seL4.