Abstract
We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison’s verification of the inference system without definitions. Soundness of the logic extends to soundness of a theorem prover, because we also show that a synthesised implementation of the kernel in CakeML refines the inference system. Apart from adding support for definitions and synthesising an implementation, we improve on Harrison’s work by making our model of HOL parametric on the universe of sets, and we prove soundness for an improved principle of constant specification in the hope of encouraging its adoption. Our semantics supports defined constants directly via a context, and we find this approach cleaner than our previous work formalising Wiedijk’s Stateless HOL.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Aït Mohamed, O., Muñoz, C. A., Tahar, S. (eds.): Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18–21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science. Springer, Berlin (2008)
Anand, A., Rahli, V.: Towards a formally verified proof assistant. In: Klein and Gamboa [15], pp. 27–44
Andrews P.B.: An Introduction to Mathematical Logic and Type Theory, Vol. 27. Springer, NY (2002)
Arthan, R.: HOL Formalised: Semantics. http://www.lemma-one.com/ProofPower/specs/spc002.pdf
Arthan, R.: HOL constant definition done right. In: Klein and Gamboa [15], pp. 531–536
Barras B.: Sets in Coq, Coq in sets. J. Formalized Reason 3(1), 29–48 (2010)
Bertot, Y.: A short presentation of Coq. In: Aït Mohamed et al. [1], pp. 12–16
Church A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940)
Gödel K: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte fr Mathematik und Physik 38(1), 173–198 (1931)
Gordon, M.: From LCF to HOL: a short history. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 169–186. The MIT Press, Cambridge (2000)
Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.), Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pp. 177–191. Springer, Berlin (2006)
Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.), TPHOLs, volume 5674 of Lecture Notes in Computer Science, pp. 60–66. Springer, Berlin (2009)
Henkin L.: Completeness in the theory of types. J. Symb. Log. 15, 81–91 (1950)
Hurd, J.: The OpenTheory standard theory library. In: Bobaru M.G., Havelund K., Holzmann, G.J., Joshi, R. (eds.), NASA Formal Methods—Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18–20, 2011. Proceedings, volume 6617 of Lecture Notes in Computer Science, pp. 177–191. Springer, Berlin (2011)
Klein, G., Gamboa, R. (eds.): 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, volume 8558 of Lecture Notes in Computer Science. Springer, Berlin (2014)
Krauss, A., Schropp, A.: A mechanized translation from higher-order logic to set theory. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pp. 323–338. Springer, Berlin (2010)
Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: HOL with definitions: Semantics, soundness, and a verified implementation. In: Klein and Gamboa [15], pp. 308–324
Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20–21, 2014, pp. 179–192. ACM, New York (2014)
Kuratowski C.: Sur la notion de l’ordre dans la théorie des ensembles. Fundam. Math. 2(1), 161–171 (1921)
Marić F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor. Comput. Sci. 411(50), 4333–4356 (2010)
Mendelson E.: Introduction to Mathematical Logic, 5th edn. CRC Press, Boca Raton, FL (2009)
Milner R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348–375 (1978)
Milner, R.: LCF: A way of doing proofs with a machine. In: Becvár, J. (eds.), Mathematical Foundations of Computer Science 1979, Proceedings, 8th Symposium, Olomouc, Czechoslovakia, September 3–7, 1979, volume 74 of Lecture Notes in Computer Science, pp. 146–159. Springer, Berlin (1979)
Myreen, M.O., Davis, J.: The reflective Milawa theorem prover is sound—(down to the machine code that runs it). In: Klein and Gamboa [15], pp. 421–436
Myreen M.O., Owens Scott: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2–3), 284–315 (2014)
Myreen, M.O., Owens, S., Kumar, R.: Steps towards verified implementations of HOL Light. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving—4th International Conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pp. 490–495. Springer, Berlin (2013)
Pitts, A.M.: The HOL System: Logic, 3rd edition. http://hol-theorem-prover.org/documentation.html
Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first-order logic. In: Hurd, J., Melham, T.F. (eds.), Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22–25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pp. 294–309. Springer, Berlin (2005)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Aït Mohamed et al. [1], pp. 28–32
VaughtRobert, L.: Set Theory: An introduction, 2nd edn. Birkhäuser, Basel (1994)
von Wright J.: Representing higher-order logic proofs in HOL. Comput. J. 38(2), 171–179 (1995)
Wang, Q., Barras, B.: Semantics of intensional type theory extended with decidable equational theories. In: Della Rocca, S.R. (ed.) Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2–5, 2013, Torino, Italy, volume 23 of LIPIcs, pp. 653–667. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik (2013)
Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Aït Mohamed et al. [1], pp. 33–38
Wiedijk, F.: Stateless HOL. In: Hirschowitz, T. (ed.) Proceedings Types for Proofs and Programs, Revised Selected Papers, TYPES 2009, Aussois, France, 12–15th May 2009, volume 53 of EPTCS, pp. 47–61 (2009)
Author information
Authors and Affiliations
Corresponding author
Additional information
The first author was supported by the Gates Cambridge Trust. The second author was funded in part by the EPSRC (Grant Number EP/K503769/1). The third author was partially supported by the Royal Society UK and the Swedish Research Council.
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Kumar, R., Arthan, R., Myreen, M.O. et al. Self-Formalisation of Higher-Order Logic. J Autom Reasoning 56, 221–259 (2016). https://doi.org/10.1007/s10817-015-9357-x
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9357-x