Skip to main content

TS

Verifying efficient function calls in CakeML

Authors

Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen

University of Kent

DATA61

Carnegie Mellon University

Chalmers University of Technology

Abstract

We have designed an intermediate language (IL) for the CakeML compiler that supports the verified, efficient compilation of functions and calls. Verified compilation steps include batching of multiple curried arguments, detecting calls to statically known functions, and specialising calls to known functions with no free variables. Finally, we verify the translation to a lower-level IL that only supports closed, first-order functions. These compilation steps resemble those found in other compilers (especially OCaml). Our contribution here is the design of the semantics of the IL, and the demonstration that our verification techniques over this semantics work well in practice at this scale. The entire development was carried out in the HOL4 theorem prover.

BibTeX Entry

  @inproceedings{Owens_NKTM_17,
    publisher        = {ACM},
    booktitle        = {International Conference on Functional Programming},
    author           = {Owens, Scott and Norrish, Michael and Kumar, Ramana and Tan, Yong Kiam and Myreen, Magnus},
    month            = sep,
    year             = {2017},
    date             = {2017-9-4},
    title            = {Verifying Efficient Function Calls in {CakeML}},
    type             = {Conference Paper - Refereed},
    pages            = {26},
    address          = {Oxford}
  }

Download

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.