Milawa swMATH ID: 9977 Software Authors: Myreen, Magnus O.; Davis, Jared Description: The reflective milawa theorem prover is sound (down to the machine code that runs it). Milawa is a theorem prover styled after ACL2 but with a small kernel and a powerful reflection mechanism. We have used the HOL4 theorem prover to formalize the logic of Milawa, prove the logic sound, and prove that the source code for the Milawa kernel (2,000 lines of Lisp) is faithful to the logic. Going further, we have combined these results with our previous verification of an x86 machine-code implementation of a Lisp runtime. Our top-level HOL4 theorem states that when Milawa is run on top of our verified Lisp, it will only print theorem statements that are semantically true. We believe that this top-level theorem is the most comprehensive formal evidence of a theorem prover’s soundness to date. Homepage: http://www.cs.utexas.edu/~jared/milawa/Web/ Related Software: HOL; Jitawa; Coq; HOL Light; Isabelle/HOL; CakeML; Isabelle; ML; OpenTheory; LCF; ACL2; HOL Zero; ProofPower; NQTHM; Agda; OCaml; GCminor; z3; CertiCoq; Nuprl Referenced in: 19 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1356.68186Davis, Jared; Myreen, Magnus O. 2015 The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1416.68174Myreen, Magnus O.; Davis, Jared 2014 all top 5 Referenced by 29 Authors 8 Myreen, Magnus O. 3 Davis, Jared 3 Kumar, Ramana 3 Owens, Scott 2 Åman Pohjola, Johannes 2 Rahli, Vincent 2 Sandberg Ericsson, Adam 1 Abrahamsson, Oskar 1 Adams, Mark 1 Anand, Abhishek 1 Arthan, Rob D. 1 Bickford, Mark 1 Cachera, David 1 Cohen, Liron 1 Demange, Delphine 1 Fallenstein, Benja 1 Gamboa, Ruben A. 1 Gauthier, Thibault 1 Jagannathan, Suresh 1 Kaliszyk, Cezary 1 Klein, Gerwin 1 Kunčar, Ondřej 1 Moore, J Strother 1 Petri, Gustavo 1 Pichardie, David 1 Popescu, Andrei 1 Schlichtkrull, Anders 1 Vitek, Jan 1 Zakowski, Yannick Referenced in 5 Serials 6 Journal of Automated Reasoning 1 Journal of Symbolic Computation 1 Formal Aspects of Computing 1 Lecture Notes in Computer Science 1 Journal of Logical and Algebraic Methods in Programming Referenced in 3 Fields 19 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) Referencing Publications by Year