Skip to main content

Proof-Producing Synthesis of CakeML from Monadic HOL Functions

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


Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (422kB) Preview
[img]
Preview
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: Faculties > Sciences > School of Computing
Depositing User: H.R. Kanabar
Date Deposited: 14 Jul 2020 16:02 UTC
Last Modified: 14 Jul 2020 16:03 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/82103 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year