Access Restriction

Author Fox, Anthony ♦ Myreen, Magnus O. ♦ Owens, Scott ♦ Kumar, Ramana ♦ Norrish, Michael ♦ Tan, Yong Kiam
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Subject Keyword Verified optimisations ♦ Compiler verification ♦ Ml
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.
Description Affiliation: Data61 at CSIRO, Australia / Australian National University, Australia (Norrish, Michael) || Data61 at CSIRO, Australia / UNSW, Australia (Kumar, Ramana) || University of Cambridge, UK (Fox, Anthony) || IHPC at A*STAR, Singapore (Tan, Yong Kiam) || University of Kent, UK (Owens, Scott) || Chalmers University of Technology, Sweden (Myreen, Magnus O.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1983-05-01
Publisher Place New York
Journal ACM SIGPLAN Notices (SIGP)
Volume Number 51
Issue Number 9
Page Count 14
Starting Page 60
Ending Page 73

Open content in new tab

   Open content in new tab
Source: ACM Digital Library