Skip to main content

CakeML: A Verified Implementation of ML

Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott (2014) CakeML: A Verified Implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL Principles of Programming Languages . ACM, New York, USA, pp. 179-191. ISBN 978-1-4503-2544-8. (doi:10.1145/2535838.2535841) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:36711)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://dx.doi.org/10.1145/2535838.2535841

Abstract

We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler bootstrapping.

Our contributions are twofold. The first is simply in building a system that is end-to-end verified, demonstrating that each piece of such a verification effort can in practice be composed with the others, and ensuring that none of the pieces rely on any over-simplifying assumptions. The second is developing novel approaches to some of the more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself: we apply the verified compiler to itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof handles diverging input programs with a lightweight approach based on logical timeout exceptions. The entire development was carried out in the HOL4 theorem prover.

Item Type: Book section
DOI/Identification number: 10.1145/2535838.2535841
Subjects: 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: Scott Owens
Date Deposited: 21 Nov 2013 13:28 UTC
Last Modified: 17 Aug 2022 10:56 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/36711 (The current URI for this page, for reference purposes)
Owens, Scott: https://orcid.org/0000-0002-7437-4780
  • Depositors only (login required):