×

A consistent foundation for Isabelle/HOL. (English) Zbl 1465.68289

Summary: The interactive theorem prover Isabelle/HOL is based on the well understood higher-order logic (HOL), which is widely believed to be consistent (and provably consistent in set theory by a standard semantic argument). However, Isabelle/HOL brings its own personal touch to HOL: overloaded constant definitions, used to provide the users with Haskell-like type classes. These features are a delight for the users, but unfortunately are not easy to get right as an extension of HOL – they have a history of inconsistent behavior. It has been an open question under which criteria overloaded constant definitions and type definitions can be combined together while still guaranteeing consistency. This paper presents a solution to this problem: non-overlapping definitions and termination of the definition-dependency relation (tracked not only through constants but also through types) ensures relative consistency of Isabelle/HOL.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B16 Higher-order logic
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] A consistent foundation for Isabelle/HOL— a correction patch. http://www21.in.tum.de/ kuncar/documents/patch.html · Zbl 1433.68556
[2] Adams, M.: Introducing HOL zero—(extended abstract). In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010, LNCS, vol. 6327, pp. 142-143. Springer (2010)
[3] Anand, A., Rahli, V.: Towards a formally verified proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 27-44. Springer (2014) · Zbl 1416.68146
[4] Arthan, R.D.: Some mathematical case studies in ProofPower-HOL. In: Slind, K. (ed.) TPHOLs 2004 (Emerging Trends), School of Computing, pp. 1-16. University of Utah (2010)
[5] Barras, B.: Coq en Coq. Tech. Rep. 3026, INRIA (1996) · Zbl 1211.03023
[6] Barras, B.: Sets in Coq Coq in Sets. J. Formaliz. Reason. 3(1), 29-48 (2010) · Zbl 1211.03023
[7] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2004) · Zbl 1069.68095 · doi:10.1007/978-3-662-07964-5
[8] Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: Fisher, K., Reppy, J.H. (eds.) ICFP 2015, pp. 192-204. ACM (2015) · Zbl 1360.68358
[9] Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda-a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009, LNCS, vol. 5674, pp. 73-78. Springer (2009) · Zbl 1252.68062
[10] Dénès, M.: [Coq-Club] Propositional extensionality is inconsistent in Coq. Archived at https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html
[11] Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)
[12] Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153-245 (2010) · Zbl 1211.68369
[13] Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006, LNCS, vol. 4502, pp. 160-174. Springer (2006) · Zbl 1178.68529
[14] Harrison, J.: HOL Light: A Tutorial Introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) FMCAD ’96, LNCS, vol. 1166, pp. 265-269. Springer (1996)
[15] Harrison, J.: Towards self-verification of HOL light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006, LNCS, vol. 4130, pp. 177-191. Springer (2006) · Zbl 1222.68364
[16] Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013, LNCS, vol. 7998, pp. 279-294. Springer (2013) · Zbl 1317.68213
[17] Huffman, B., Urban, C.: A New Foundation for Nominal Isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010, LNCS, vol. 6172, pp. 35-50. Springer (2010) · Zbl 1291.68350
[18] Krauss, A., Schropp, A.: A Mechanized translation from higher-order logic to set theory. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010, LNCS, vol. 6172, pp. 323-338. Springer (2010) · Zbl 1291.68355
[19] 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, vol. 8558, pp. 308-324. Springer (2014) · Zbl 1416.68167
[20] Kunčar, O.: Correctness of Isabelle’s cyclicity checker: implementability of overloading in proof assistants. In: Leroy, X., Tiu, A. (eds.) CPP 2015, pp. 85-94. ACM (2015)
[21] Kunčar, O., Popescu, A.: A consistent foundation for Isabelle/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015, LNCS, vol. 9236, pp. 234-252. Springer (2015) · Zbl 1433.68556
[22] Kunčar, O., Popescu, A.: Comprehending Isabelle/HOL’s consistency. In: Yang, H. (ed.) ESOP 2017, LNCS, vol. 10201, pp. 724-749. Springer (2017) · Zbl 1485.68285
[23] Kunčar, O., Popescu, A.: Safety and conservativity of definitions in hol and isabelle/hol (2018). Conditionally accepted at POPL 2018. Draft available at http://andreipopescu.uk/pdf/conserv_HOL_IsabelleHOL.pdf
[24] Leino, K.R.M., Moskal, M.: Co-induction simply—automatic co-inductive proofs in a program verifier. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014, LNCS, vol. 8442, pp. 382-398. Springer (2014)
[25] Lochbihler, A.: Light-weight containers for Isabelle: efficient, extensible, nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013, LNCS, vol. 7998, pp. 116-132. Springer (2013) · Zbl 1317.68219
[26] McBride, C., et al.: [HoTT] Newbie questions about homotopy theory and advantage of UF/Coq. Archived at http://article.gmane.org/gmane.comp.lang.agda/6106
[27] Müller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF= HOL+LCF. J. Funct. Program. 9(2), 191-223 (1999) · Zbl 0933.03028 · doi:10.1017/S095679689900341X
[28] Myreen, M.O., Davis, J.: The reflective Milawa theorem prover is sound—(down to the machine code that runs it). In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 421-436. Springer (2014) · Zbl 1416.68174
[29] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a proof assistant for higher-order logic, LNCS, vol. 2283, Springer (2002) · Zbl 0994.68131
[30] Nipkow, T., Snelting, G.: Type classes and overloading resolution via order-sorted unification. In: Hughes, J. (ed.) Functional Programming Languages and Computer Architecture, LNCS, vol. 523, pp. 1-14. Springer (1991)
[31] Obua, S.: Checking conservativity of overloaded definitions in higher-order logic. In: Pfenning, F. (ed.) RTA 2006, LNCS, vol. 4098, pp. 212-226. Springer (2006) · Zbl 1151.68637
[32] Pitts, A.: Introduction to HOL: a theorem proving environment for higher order logic, chap. The HOL Logic. In: Gordon and Melham [12] pp. 191-232. (1993)
[33] Shankar, N., Owre, S., Rushby, J.M.: PVS Tutorial. Computer Science Laboratory, SRI International (1993). http://www.csl.sri.com/papers/wift-tutorial/
[34] Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2008, LNCS, vol. 5170, pp. 278-293. Springer (2008) · Zbl 1165.68475
[35] Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327-356 (2008) · Zbl 1140.68061 · doi:10.1007/s10817-008-9097-2
[36] The HOL4 Theorem Prover. http://hol.sourceforge.net/
[37] Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: POPL ’89, pp. 60-76. ACM (1989)
[38] Wenzel, M.: Type Classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs ’97, LNCS, vol. 1275, pp. 307-322. Springer (1997)
[39] Wenzel, M.: The Isabelle/Isar Reference Manual (2016). http://isabelle.in.tum.de/doc/isar-ref.pdf
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.