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 34 articles )

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

1 2 next

  1. Fava, Daniel S.; Steffen, Martin; Stolz, Volker: Operational semantics of a weak memory model with channel synchronization (2019)
  2. Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)
  3. Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes: A verified generational garbage collector for CakeML (2019)
  4. Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
  5. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  6. Ho, Son; Abrahamsson, Oskar; Kumar, Ramana; Myreen, Magnus O.; Tan, Yong Kiam; Norrish, Michael: Proof-producing synthesis of cakeml with I/O and local state from monadic HOL functions (2018)
  7. Hupel, Lars; Nipkow, Tobias: A verified compiler from Isabelle/HOL to CakeML (2018)
  8. Immler, Fabian: A verified ODE solver and the Lorenz attractor (2018)
  9. Jantsch, Simon; Norrish, Michael: Verifying the LTL to Büchi automata translation via very weak alternating automata (2018)
  10. Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O.: Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (2018)
  11. Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
  12. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
  13. Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
  14. Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
  15. Rahli, Vincent; Cohen, Liron; Bickford, Mark: A verified theorem prover backend supported by a monotonic library (2018)
  16. Rizkallah, Christine; Garbuzov, Dmitri; Zdancewic, Steve: A formal equational theory for call-by-push-value (2018)
  17. 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)
  18. Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael: Verified characteristic formulae for CakeML (2017)
  19. Pattinson, Dirk; Tiwari, Mukesh: Schulze voting as evidence carrying computation (2017)
  20. Rosemann, Julian; Schneider, Sigurd; Hack, Sebastian: Verified spilling and translation validation with repair (2017)

1 2 next