Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Date
2018
Authors
Ho, Son
Abrahamsson, Oskar
Kumar, Ramana
Myreen, Magnus
Tan, Yong Kiam
Norrish, Michael
Journal Title
Journal ISSN
Volume Title
Publisher
Springer Verlag
Abstract
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 type inferencer and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.
Description
Keywords
Citation
Collections
Source
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2099-12-31
Downloads
File
Description