Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Mon 19 Sep 2016 13:40 - 14:05 at Noh Theater - Session 2 Chair(s): Kathleen Fisher

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.

Mon 19 Sep
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

13:40 - 14:55: Session 2Research Papers at Noh Theater
Chair(s): Kathleen FisherTufts University
13:40 - 14:05
Talk
A New Verified Compiler Backend for CakeML
Research Papers
Yong Kiam TanIHPC at A*STAR, Singapore, Magnus O. MyreenChalmers University of Technology, Sweden, Ramana KumarData61 at CSIRO, Australia, Anthony FoxUniversity of Cambridge, UK, Scott OwensUniversity of Kent, UK, Michael NorrishData61 at CSIRO, Australia
DOI
14:05 - 14:30
Talk
Sequent Calculus as a Compiler Intermediate Language
Research Papers
Paul DownenUniversity of Oregon, USA, Luke MaurerUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft Research, UK
DOI
14:30 - 14:55
Talk
Refinement through Restraint: Bringing Down the Cost of Verification
Research Papers
Liam O'ConnorUNSW, Australia, Zilin ChenUNSW, Australia, Christine RizkallahUniversity of Pennsylvania, USA, Sidney AmaniUNSW, Australia, Japheth LimData61, Australia, Toby MurrayUniversity of Melbourne, Australia, Yutaka NagashimaData61, Australia, Thomas SewellUNSW, Australia, Gerwin KleinUNSW, Australia
DOI