The verified CakeML compiler backend
-
Altmetric Citations
Tan, Yong Kiam; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael
Description
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 compiler's implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports...[Show more]
Collections | ANU Research Publications |
---|---|
Date published: | 2019-02-04 |
Type: | Journal article |
URI: | http://hdl.handle.net/1885/309731 |
Source: | Journal of Functional Programming |
DOI: | 10.1017/S0956796818000229 |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
the-verified-cakeml-compiler-backend.pdf | 867.22 kB | Adobe PDF | Request a copy |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator