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 machinecode implementation of a Lisp runtime. Our toplevel 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 toplevel 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 
Cited 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.68186 Davis, Jared; Myreen, Magnus O. 
2015

The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1416.68174 Myreen, Magnus O.; Davis, Jared 
2014

all
top 5
Cited by 29 Authors
Cited 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 
Cited in 3 Fields
19  Computer science (68XX) 
5  Mathematical logic and foundations (03XX) 
1  General and overarching topics; collections (00XX) 