Abrahamsson, Oskar, Ho, Son, Kanabar, Hrutvik, Kumar, Ramana, Myreen, Magnus O., Norrish, Michael, Tan, Yong Kiam (2020) Proof-Producing Synthesis of CakeML from Monadic HOL Functions. Journal of Automated Reasoning, . ISSN 0168-7433. (doi:10.1007/s10817-020-09559-8) (KAR id:82103)
PDF
Publisher pdf
Language: English
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
Download this file (PDF/401kB) |
|
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: https://doi.org/10.1007/s10817-020-09559-8 |
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 instruction encoder 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.
Item Type: | Article |
---|---|
DOI/Identification number: | 10.1007/s10817-020-09559-8 |
Uncontrolled keywords: | Interactive theorem proving; Program synthesis; ML; Higher-order logic |
Subjects: |
Q Science Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Hrutvik Kanabar |
Date Deposited: | 14 Jul 2020 16:02 UTC |
Last Modified: | 10 Dec 2022 13:20 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/82103 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):