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.

References in zbMATH (referenced in 17 articles )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Ayala-Rincón, Mauricio (ed.); Muñoz, César A. (ed.): Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (2017)
  2. Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael: Verified characteristic formulae for CakeML (2017)
  3. Pattinson, Dirk; Tiwari, Mukesh: Schulze voting as evidence carrying computation (2017)
  4. Rosemann, Julian; Schneider, Sigurd; Hack, Sebastian: Verified spilling and translation validation with repair (2017)
  5. Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes: A verified generational garbage collector for CakeML (2017)
  6. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2016)
  7. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
  8. Rizkallah, Christine; Lim, Japheth; Nagashima, Yutaka; Sewell, Thomas; Chen, Zilin; O’Connor, Liam; Murray, Toby; Keller, Gabriele; Klein, Gerwin: A framework for the automatic formal verification of refinement from cogent to C (2016)
  9. Wang, Yuting; Nadathur, Gopalan: A higher-order abstract syntax approach to verified transformations on functional programs (2016)
  10. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  11. Fox, Anthony: Improved tool support for machine-code decompilation in HOL4 (2015)
  12. Théry, Laurent (ed.); Wiedijk, Freek (ed.): Foreword to the special focus on formal proofs for mathematics and computer science (2015)
  13. Anand, Abhishek; Rahli, Vincent: Towards a formally verified proof assistant (2014)
  14. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: HOL with definitions: semantics, soundness, and a verified implementation (2014)
  15. Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott: Cakeml, a verified implementation of ML (2014)
  16. Mulligan, Dominic P.; Owens, Scott; Gray, Kathryn E.; Ridge, Tom; Sewell, Peter: Lem: reusable engineering of real-world semantics (2014)
  17. Myreen, Magnus O.; Davis, Jared: The reflective milawa theorem prover is sound (down to the machine code that runs it) (2014)