×

The reflective Milawa theorem prover is sound (down to the machine code that runs it). (English) Zbl 1416.68174

Klein, Gerwin (ed.) et al., Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 421-436 (2014).
Summary: 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.
For the entire collection see [Zbl 1294.68020].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Milawa; HOL; CakeML; ACL2; Coq; Jitawa
PDFBibTeX XMLCite
Full Text: DOI