Trustworthy Systems

Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions

Authors

Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus Myreen, Yong Kiam Tan and Michael Norrish

Carnegie Mellon University

DATA61

MINES ParisTech

DeepMind

Chalmers University of Technology

Australian National University

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 type inferencer 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.

BibTeX Entry

  @inproceedings{Ho_AKMTN_18,
    address          = {Oxford},
    author           = {Ho, Son and Abrahamsson, Oskar and Kumar, Ramana and Myreen, Magnus and Tan, Yong Kiam and Norrish,
                        Michael},
    booktitle        = {International Joint Conference on Automated Reasoning},
    date             = {2018-7-14},
    doi              = {https://doi.org/10.1007/978-3-319-94205-6\_42},
    editor           = {{Didier Galmiche and Stephan Schulz and Roberto Sebastiani}},
    month            = jul,
    pages            = {646-662},
    paperurl         = {https://trustworthy.systems/publications/full_text/Ho_AKMTN_18.pdf},
    publisher        = {Springer},
    title            = {Proof-Producing Synthesis of {CakeML} with {I}/{O} and Local State from Monadic {HOL} Functions},
    year             = {2018}
  }

Download