Proof-Producing Synthesis of CakeML from Monadic HOL Functions

Oskar Abrahamsson; Son Ho; Hrutvik Kanabar; Ramana Kumar; Magnus O. Myreen; Michael Norrish; Yong Kiam Tan

doi:10.1007/s10817-020-09559-8

Proof-Producing Synthesis of CakeML from Monadic HOL Functions

Oskar Abrahamsson^*, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

8 Citations (Scopus)

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.

Original language	English
Pages (from-to)	1287-1306
Number of pages	20
Journal	Journal of Automated Reasoning
Volume	64
Issue number	7
DOIs	https://doi.org/10.1007/s10817-020-09559-8
Publication status	Published - 1 Oct 2020
Externally published	Yes

Access to Document

10.1007/s10817-020-09559-8

Cite this

@article{ac47373f4d264978b3d1c7e281cc9f78,

title = "Proof-Producing Synthesis of CakeML from Monadic HOL Functions",

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.",

keywords = "Higher-order logic, Interactive theorem proving, ML, Program synthesis",

author = "Oskar Abrahamsson and Son Ho and Hrutvik Kanabar and Ramana Kumar and Myreen, {Magnus O.} and Michael Norrish and Tan, {Yong Kiam}",

note = "Publisher Copyright: {\textcopyright} 2020, The Author(s).",

year = "2020",

month = oct,

day = "1",

doi = "10.1007/s10817-020-09559-8",

language = "English",

volume = "64",

pages = "1287--1306",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "7",

}

TY - JOUR

T1 - Proof-Producing Synthesis of CakeML from Monadic HOL Functions

AU - Abrahamsson, Oskar

AU - Ho, Son

AU - Kanabar, Hrutvik

AU - Kumar, Ramana

AU - Myreen, Magnus O.

AU - Norrish, Michael

AU - Tan, Yong Kiam

PY - 2020/10/1

Y1 - 2020/10/1

N2 - 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.

AB - 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.

KW - Higher-order logic

KW - Interactive theorem proving

KW - ML

KW - Program synthesis

UR - http://www.scopus.com/inward/record.url?scp=85086123435&partnerID=8YFLogxK

U2 - 10.1007/s10817-020-09559-8

DO - 10.1007/s10817-020-09559-8

M3 - Article

SN - 0168-7433

VL - 64

SP - 1287

EP - 1306

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 7

ER -

Proof-Producing Synthesis of CakeML from Monadic HOL Functions

Abstract

Access to Document

Other files and links

Fingerprint

Cite this