CakeML swMATH ID: 8799 Software Authors: Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott Description: 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. Homepage: https://cakeml.org/ Keywords: ML; compiler bootstrapping; compiler verification; machine code verification; read-eval-print loop; verified garbage collection; verified parsing; verified type checking Related Software: Isabelle/HOL; Coq; HOL; HOL Light; seL4; Isabelle; CertiCoq; Archive Formal Proofs; Sledgehammer; Milawa; Jitawa; CompCert; OpenTheory; OEuf; CAVA LTL Modelchecker; kepler98; OCaml; Flyspeck; Nitpick; ACL2 Cited in: 58 Publications all top 5 Cited by 102 Authors 14 Myreen, Magnus O. 9 Kumar, Ramana 6 Norrish, Michael 5 Nipkow, Tobias 5 Owens, Scott 4 Tan, Yong Kiam 3 Abrahamsson, Oskar 3 Klein, Gerwin 3 Murray, Toby 3 Paulson, Lawrence Charles 3 Popescu, Andrei 3 Rizkallah, Christine 3 Sutcliffe, Geoff 2 Åman Pohjola, Johannes 2 Arthan, Rob D. 2 Bauereiß, Thomas 2 Chen, Zilin 2 Davis, Jared 2 Fox, Anthony C. J. 2 Heule, Marijn J. H. 2 Ho, Son Lam 2 Keller, Gabriele Cornelia 2 Lammich, Peter 2 Lim, Japheth 2 Lochbihler, Andreas 2 Nagashima, Yutaka 2 O’Connor, Liam 2 Pesenti Gritti, Armando 2 Rahli, Vincent 2 Raimondi, Franco 2 Roßkopf, Simon 2 Sandberg Ericsson, Adam 2 Sewell, Thomas D. 2 Wenzel, Makarius 1 Abel, Andreas M. 1 Allais, Guillaume 1 Amani, Sidney 1 Anand, Abhishek 1 Annenkov, Danil 1 Avigad, Jeremy 1 Ayala-Rincón, Mauricio 1 Baek, Seulkee 1 Bickford, Mark 1 Blanchette, Jasmin Christian 1 Brinkop, Hauke 1 Brown, Chad Edward 1 Chakravarty, Manuel M. T. 1 Cohen, Liron 1 Dam, Mads 1 Fava, Daniel Schnetzer 1 Garbuzov, Dmitri 1 Gauthier, Thibault 1 Gray, Kathryn E. 1 Guanciale, Roberto 1 Guéneau, Armaël 1 Hack, Sebastian 1 Hameer, Aliya 1 Hayes, Ian J. 1 Hou, Ping 1 Hupel, Lars 1 Immler, Fabian 1 Jantsch, Simon 1 Kaliszyk, Cezary 1 Kanabar, Hrutvik 1 Korovin, Konstantin 1 Krijnen, Jacco O. G. 1 Lindner, Andreas 1 López-Hernández, Julio César 1 Lundberg, Didrik 1 Mahboubi, Assia 1 Milo, Mikkel 1 Momigliano, Alberto 1 Mullen, Eric 1 Mulligan, Dominic P. 1 Muñoz, César A. 1 Nadathur, Gopalan 1 Nielsen, Jakob Botsch 1 Pattinson, Dirk 1 Pientka, Brigitte 1 Ridge, Thomas 1 Rosemann, Julian 1 Schäfer, Steven 1 Schneider, Sigurd 1 Sewell, Peter 1 Sibut-Pinote, Thomas 1 Sison, Robert 1 Snelting, Gregor 1 Spitters, Bas 1 Stark, Kathrin 1 Steffen, Martin 1 Stolz, Volker 1 Swierstra, Wouter 1 Tatlock, Zachary 1 Théry, Laurent 1 Tiwari, Mukesh 1 Tuerk, Thomas 1 Urban, Josef 1 Utting, Mark 1 Wang, Yuting 1 Webb, Brae J. ...and 2 more Authors all top 5 Cited in 10 Serials 12 Journal of Automated Reasoning 4 Journal of Functional Programming 2 AI Communications 2 Logical Methods in Computer Science 2 Journal of Logical and Algebraic Methods in Programming 1 Formal Aspects of Computing 1 Lecture Notes in Computer Science 1 Mathematics in Computer Science 1 Journal of Formalized Reasoning 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 8 Fields 58 Computer science (68-XX) 10 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Numerical analysis (65-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year