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.
Keywords for this software
References in zbMATH (referenced in 11 articles , 2 standard articles )
Showing results 1 to 11 of 11.
- Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes: A verified generational garbage collector for CakeML (2017)
- Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- Anand, Abhishek; Rahli, Vincent: Towards a formally verified proof assistant (2014)
- Klein, Gerwin (ed.); Gamboa, Ruben (ed.): 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 (2014)
- Myreen, Magnus O.; Davis, Jared: The reflective milawa theorem prover is sound (down to the machine code that runs it) (2014)
- Myreen, Magnus O.; Owens, Scott; Kumar, Ramana: Steps towards verified implementations of HOL Light (2013)
- Myreen, Magnus O.: Functional programs: conversions between deep and shallow embeddings (2012) ioport
- Myreen, Magnus O.; Owens, Scott: Proof-producing synthesis of ML from higher-order logic (2012)
- Myreen, Magnus O.; Davis, Jared: A verified runtime for a verified theorem prover (2011)