Proof-Producing Synthesis of CakeML from Monadic HOL Functions
-
Altmetric Citations
Abrahamsson, Oskar; Ho, Son; Kanabar, Hrutvik; Kumar, Ramana; Myreen, Magnus; Norrish, Michael; Tan, Yong Kiam
Description
We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better...[Show more]
Collections | ANU Research Publications |
---|---|
Date published: | 2020 |
Type: | Journal article |
URI: | http://hdl.handle.net/1885/311302 |
Source: | Journal of Automated Reasoning |
DOI: | 10.1007/s10817-020-09559-8 |
Access Rights: | Open Access |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
s10817-020-09559-8.pdf | 381.4 kB | Adobe PDF |
This item is licensed under a Creative Commons License
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator