Cakeml, a verified implementation of ML. 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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- Fox, Anthony: Improved tool support for machine-code decompilation in HOL4 (2015)
- Théry, Laurent (ed.); Wiedijk, Freek (ed.): Foreword to the special focus on formal proofs for mathematics and computer science (2015)
- Anand, Abhishek; Rahli, Vincent: Towards a formally verified proof assistant (2014)
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: HOL with definitions: semantics, soundness, and a verified implementation (2014)
- Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott: Cakeml, a verified implementation of ML (2014)
- Mulligan, Dominic P.; Owens, Scott; Gray, Kathryn E.; Ridge, Tom; Sewell, Peter: Lem: reusable engineering of real-world semantics (2014)
- Myreen, Magnus O.; Davis, Jared: The reflective milawa theorem prover is sound (down to the machine code that runs it) (2014)