Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barras, B.: Sets in Coq, Coq in sets. J. Formalized Reasoning 3(1) (2010)
Davis, J.C.: A Self-Verifying Theorem Prover. PhD thesis, University of Texas at Austin (December 2009)
Gordon, M.J.C., Hunt Jr., W.A., Kaufmann, M., Reynolds, J.: An embedding of the ACL2 logic in HOL. In: International Workshop on the ACL2 Theorem Prover and its Applications (ACL2), pp. 40–46. ACM (2006)
Gordon, M.J.C., Reynolds, J., Hunt Jr., W.A., Kaufmann, M.: An integration of HOL and ACL2. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 153–160. IEEE Computer Society (2006)
Harrison, J.: HOL light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009)
Kaufmann, M., Manolios, P., Strother Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (June 2000)
Kaufmann, M., Slind, K.: Proof pearl: Wellfounded induction on the ordinals up to ε 0. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 294–301. Springer, Heidelberg (2007)
Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: HOL with Definitions: Semantics, Soundness, and a Verified Implementation. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS (LNAI), vol. 8558, pp. 302–317. Springer, Heidelberg (2014)
Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Sewell, P. (ed.) Principles of Programming Languages (POPL). ACM (2014)
Marić, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor. Comput. Sci. 411(50) (2010)
Myreen, M.O.: Verified just-in-time compiler on x86. In: Hermenegildo, M.V., Palsberg, J. (eds.) Principles of Programming Languages (POPL). ACM (2010)
Myreen, M.O.: Functional programs: Conversions between deep and shallow embeddings. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 412–417. Springer, Heidelberg (2012)
Myreen, M.O., Davis, J.: A verified runtime for a verified theorem prover. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 265–280. Springer, Heidelberg (2011)
Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 294–309. Springer, Heidelberg (2005)
Wang, Q., Barras, B.: Semantics of intensional type theory extended with decidable equational theories. In: Computer Science Logic (CSL). LIPIcs, vol. 23. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Myreen, M.O., Davis, J. (2014). The Reflective Milawa Theorem Prover Is Sound. In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_27
Download citation
DOI: https://doi.org/10.1007/978-3-319-08970-6_27
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08969-0
Online ISBN: 978-3-319-08970-6
eBook Packages: Computer ScienceComputer Science (R0)