CakeML
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 49 articles )
Showing results 1 to 20 of 49.
Sorted by year (- Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
- Popescu, Andrei; Lammich, Peter; Hou, Ping: CoCon: a conference management system with formally verified document confidentiality (2021)
- Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
- Abrahamsson, Oskar; Ho, Son; Kanabar, Hrutvik; Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Tan, Yong Kiam: Proof-producing synthesis of CakeML from monadic HOL functions (2020)
- Carneiro, Mario: Metamath Zero: designing a theorem prover prover (2020)
- Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
- Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
- Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
- Fava, Daniel S.; Steffen, Martin; Stolz, Volker: Operational semantics of a weak memory model with channel synchronization (2019)
- Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael: The verified CakeML compiler backend (2019)
- Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes: A verified generational garbage collector for CakeML (2019)
- 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)
- Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
- 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)
- Hupel, Lars; Nipkow, Tobias: A verified compiler from Isabelle/HOL to CakeML (2018)
- Immler, Fabian: A verified ODE solver and the Lorenz attractor (2018)
- Jantsch, Simon; Norrish, Michael: Verifying the LTL to Büchi automata translation via very weak alternating automata (2018)
- 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)