CakeML: A Verified Implementation of ML

Select |




Print


Kumar, Ramana; Myreen, Magnus; Norrish, Michael; Owens, Scott

Kumar, Ramana; Myreen, Magnus; Norrish, Michael; Owens, Scott


2014-01-22


Conference Material


ACM-SIGACT Symposium on Principles of Programming Languages (POPL)


San Diego


179--191


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, according to our model of x86-64, whatever results are printed at the REPL are permitted by the semantics of CakeML. Thus, 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.


ACM Press


SML, theorem-proving, verification


https://doi.org/10.1145/2535838.2535841


http://popl.mpi-sws.org/2014/


Copyright is held by the owner/author(s). Publication rights licensed to ACM. ACM 978-1-4503-2544-8/14/01


nicta:7494


Kumar, Ramana; Myreen, Magnus; Norrish, Michael; Owens, Scott. CakeML: A Verified Implementation of ML. In: Peter Sewell Editor, editor/s. ACM-SIGACT Symposium on Principles of Programming Languages (POPL); San Diego. ACM Press; 2014-01-22. 179--191. https://doi.org/10.1145/2535838.2535841



Loading citation data...

Citation counts
(Requires subscription to view)