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 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:	05 Nov 2024 12:48 UTC
Resource URI:	https://kar.kent.ac.uk/id/eprint/82103 (The current URI for this page, for reference purposes)

University of Kent Author Information

Kanabar, Hrutvik.

Creator's ORCID:
CReDIT Contributor Roles:

Depositors only (login required):

Altmetric

Download Statistics

Total unique views for this document in KAR since July 2020. For more details click on the image.