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

Click to download this file (401kB)
[thumbnail of s10817-020-09559-8.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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: (The current URI for this page, for reference purposes)
  • Depositors only (login required):

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