A new verified compiler backend for CakeML

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


    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.
    Original languageEnglish
    Title of host publicationProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
    EditorsJacques Garrigue, Gabriele Keller,
    Place of PublicationUSA
    PublisherAssociation for Computing Machinery (ACM)
    ISBN (Print)978-1-4503-4219-3
    Publication statusPublished - 2016
    EventICFP'16: ACM SIGPLAN International Conference on Functional Programming - Nara, Japan
    Duration: 1 Jan 2016 → …


    ConferenceICFP'16: ACM SIGPLAN International Conference on Functional Programming
    Period1/01/16 → …
    OtherSeptember 18 - 24


    Dive into the research topics of 'A new verified compiler backend for CakeML'. Together they form a unique fingerprint.

    Cite this