Abstract
Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today’s powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing techniques from the world of first order theorem proving, but also the automatic search for counterexamples. They include a highly readable structured language of proofs and a unique interactive development environment for editing live proof documents. Everything rests on the foundation conceived by Robin Milner for Edinburgh LCF: a proof kernel, using abstract types to ensure soundness and eliminate the need to store proofs. Compared with the research prototypes of the 1970s, Isabelle is a practical and versatile tool. It is used by system designers, mathematicians and many others.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Antoy, S., Hanus, M.: Functional logic programming. Commun ACM 53(4), 74–85 (2010)
Arthan, R.: On definitions of constants and types in HOL. J Autom Reason 56(3), 205–219 (2016)
Aspinall D (2000) Proof general: a generic tool for proof development. In: Graf S, Schwartzbach M (eds) European joint conferences on theory and practice of software (ETAPS), vol 1785 of LNCS. Springer
Ballarin C (2006) Interpretation of locales in Isabelle: theories and proof contexts. In: Borwein JM, Farmer WM (eds) 5th international conference mathematical knowledge management, MKM 2006, vol 4108 of Lecture notes in computer science. Springer, pp 31–43
Ballarin, C.: Locales: a module system for mathematical theories. J Autom Reason 52(2), 123–153 (2014)
Barwise J (1977) An introduction to first-order logic. In: Barwise J (ed) Handbook of mathematical logic. North-Holland, pp 5–46
Bancerek, G., Bylinski, C., Grabowski, A., Kornilowicz, A., Matuszewski, R., Naumowicz, A., Pak, K.: The role of the mizar mathematical library for interactive proof development in Mizar. J Autom Reason 61(1–4), 9–32 (2018)
Berghofer S, Bulwahn L, Haftmann F (2009) Turning inductive into equational specifications. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Theorem proving in higher order logics, vol 5674 of LNCS. Springer, pp 131–146
Blanchette JC, Bulwahn L, Nipkow T (2011) Automatic proof and disproof in Isabelle/HOL. In: Tinelli C, Sofronie- Stokkermans V (eds) Frontiers of combining systems (FroCoS 2011), vol 6989 of LNCS. Springer, pp 12–27
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J Autom Reason 51(1), 109–128 (2013)
Bertot Y, Castéran P (2004) Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer
Bulwahn L, Krauss A, Haftmann F, Erkök L, Matthews J (2008) Imperative functional programming with Isabelle/HOL. In: Mohamed OA, Muñoz CA, Tahar S (eds) 21st international conference theorem proving in higher order logics, TPHOLs 2008. vol 5170 of Lecture notes in computer science. Springer, pp 134–149
Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. J Autom Reason 60(1), 3–21 (2018)
Blanchette JC (2012) Automatic proofs and refutations for higher-order logic. PhD thesis, Technical University Munich
Blanchette, J.C.: Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. Softw Qual J 21(1), 101–126 (2013)
Boyer RS, Moore JS (1979) A computational logic. Academic Press
Berghofer S, Nipkow T (2002) Executing higher order logic. In: Callaghan P, Luo Z, McKinna J, Pollack R (eds) Types for proofs and programs (TYPES 2000), vol 2277 of LNCS. Springer, pp 24–40
Berghofer S, Nipkow T (2004) Random testing in Isabelle/HOL. In: Cuellar J, Liu Z (eds) Software engineering and formal methods (SEFM 2004). IEEE Computer Society, pp 230–239
Blanchette JC,NipkowT (2010)Nitpick: a counterexample generator for higher-order logic based on a relationalmodel finder. In: Kaufmann M, Paulson LC (eds) Interactive theorem proving, vol 6172 of LNCS. Springer, pp 131–146
Bulwahn L (2012) Counterexample generation for higher-order logic using functional and logic programming. PhD thesis, Technical University Munich
Bulwahn L (2012) The new quickcheck for Isabelle: random, exhaustive and symbolic testing under one roof. In: Hawblitzel C, Miller D (eds) Certified programs and proofs, vol 7679 of LNCS. Springer, pp 92–108
Bulwahn L (2012) Smart testing of functional programs in Isabelle. In: Bjørner N, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning, vol 7180 of LNCS. Springer, pp 153–167
Chamarthi HR, Dillinger PC, Kaufmann M, Manolios P (2011) Integrating testing and interactive theorem proving. In: Hardin D, Schmaltz J (eds) 10th international workshop on the ACL2 theorem prover and its applications, ACL2 2011, vol 70 of EPTCS, pp 4–19
Claessen K, Hughes J (2000) QuickCheck: a lightweight tool for random testing of Haskell programs. In: Odersky M, Wadler P (eds) Fifth ACM SIGPLAN international conference on functional programming (ICFP '00). ACM, pp 268–279
Clocksin WF, Mellish CS (1987) Programming in prolog, 3rd edn. Springer
Dybjer P, Haiyan Q, Takeyama M (2003) Combining testing and proving in dependent type theory. In: Theorem proving in higher order logics, vol 2758 of LNCS. Springer, pp 188–203
Divasón J, Joosten SJC, Kuncar O, Thiemann R, Yamada A (2018) Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper). In: Andronick J, Felty AP (eds) 7th ACM SIGPLAN international conference on certified programs and proofs, CPP 2018. ACM, pp 2–13
Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Published online, J Autom Reason (2019)
de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan C, Rehof J (eds) Tools and algorithms for the construction and analysis of systems, vol 4963 of Lecture notes in computer science. Springer, pp 337–340
de Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated deduction–CADE-25. Lecture notes in computer science, vol. 9195, pp. 378–388. Springer (2015)
Debray, S.K., Warren, D.S.: Automatic mode inference for logic programs. J Log Program 5(3), 207–229 (1988)
Eberl M (2015) A decision procedure for univariate real polynomials in Isabelle/HOL. In: 2015 conference on certified programs and proofs, CPP '15. ACM, pp 75–83
Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) 25th international conference computer aided verification, CAV 2013. Lecture notes in computer science, vol. 8044, pp. 463–478. Springer (2013)
Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. 12th ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL), pp. 52–66. New York, NY, USA. ACM (1985)
Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J Autom Reason 58(1), 3–31 (2017)
Griffioen, D., Huisman, M.: A comparison of PVS and Isabelle/HOL. In: Grundy, J., Newey, M. (eds.) Theorem proving in higher order logics: TPHOLs '98, pp. 123–142. Springer (1998)
Gomes VBF, Kleppmann M, Mulligan DP, Beresford AR (2017) Verifying strong eventual consistency in distributed systems. Proc ACM Program Lang 1(OOPSLA):109:1–109:28
Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J Autom Reason 55(3), 191–198 (2015)
Gordon MJC, Melham TF (eds) (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press
Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J Formaliz Reason 3(2), (2010)
Gordon MJC, Milner R, Wadsworth CP (1979) Edinburgh LCF: a mechanised logic of computation. LNCS 78. Springer
Goguen, J.A.: Some design principles and theory for OBJ-O, a language to express and execute algebraic specification for programs. In: Blum, E.K., Paul, M., Takasu, S. (eds.) Mathematical studies of information processing, vol 75 of LNCS, pp. 425–473. Springer (1979)
Gordon, M.J.C.: Why higher-order logic is a good formalism for specifying and verifying hardware. In: Milne, G., Subrahmanyam, P.A. (eds.) Formal aspects of VLSI design, pp. 153–177. North-Holland (1986)
Gordon, M.J.C.: From LCF to HOL: a short history. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, language, and interaction: essays in honor of Robin Milner, pp. 169–185. MIT Press (2000)
Gordon, M.J.C.: Tactics for mechanized reasoning: a commentary on Milner (1984) The use of machines to assist in rigorous proof. Philos Trans R Soc Ser A 373(2039), (2015)
Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T., et al.: A formal proof of the Kepler conjecture. Forum Math Pi 5, e2 (2017)
Haftmann F (2009) Code generation from specifications in higher order logic. PhD thesis, Technische Universität München
Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) Formal methods in computer-aided design: FMCAD '96, LNCS 1166, pp. 265–269. Springer (1996)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J ACM 40(1), 143–184 (1993)
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.) 4th international conference interactive theorem proving, LNCS 7998, pp. 279–294. Springer (2013)
Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) 4th international conference interactive theorem proving, vol 7998 of LNCS, pp. 100–115. Springer (2013)
Hunt Jr., W.A., Matt, K., Strother, M.J., Anna, S.: Industrial hardware and software verification with ACL2. Philos Trans R Soc Ser A 375(2104), (2017)
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and logic programming (FLOPS 2010), vol 6009 of LNCS, pp. 103–117. Springer (2010)
Hupel, L., Nipkow, T.: A verified compiler from Isabelle/HOL to CakeML. In: Ahmed, A. (ed.) European symposium on programming (ESOP 2018), vol 10801 of LNCS, pp. 999–1026. Springer (2018)
Hoffmann Christoph, M., O'Donnell Michael, J.: Programming with equations. ACM Trans Program Lang Syst 4(1), 83–112 (1982)
Holzmann, G.J.: The model checker SPIN. IEEE Trans Softw Eng 23(5), 279–295 (1997)
Huet, G.P.: A unification algorithm for typed \(\lambda \)-calculus. Theor Comput Sci 1, 27–57 (1975)
Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for proofs and programs, vol 4502 of LNCS, pp. 160–174. Springer (2006)
Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle/Isar. In: Berardi, S., Damiani, F., de Liguoro, U. (eds.) Types for proofs and programs, TYPES 2008, vol 5497 of LNCS. Springer (2009)
Jackson D (2006) Software abstractions. Logic, language, and analysis. MIT Press
Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: sel4: formal verification of an operating-system kernel. Commun ACM 53(6), 107–115 (2010)
Kalvala S (1991) HOL around the world. In: Archer M, Joyce JJ, Levitt KN, Windley PJ (eds) International workshop on the HOL theorem proving system and its applications. IEEE Computer Society, pp 4–12
Kumar R, Myreen MO, Norrish M, Owens S (2014) 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. ACM, pp 179–192
Kunčar O, Popescu A (2018) Safety and conservativity of definitions in HOL and Isabelle/HOL. PACMPL 2(POPL):24:1–24:26
Kunčar, O., Popescu, A.: A consistent foundation for Isabelle/HOL. J. Autom Reason 62(4), 531–555 (2019)
Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Thery, L. (eds.) Theorem proving in higher order logics: TPHOLs '99, vol 1690 of LNCS. Springer (1999)
Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) 4th international conference interactive theorem proving ITP 2013. Lecture notes in computer science, vol. 7998, pp. 84–99. Springer (2013)
Lammich, P.: Verified efficient implementation of Gabow's strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) 5th international conference interactive theorem proving ITP 2014. Lecture notes in computer science, vol. 8558, pp. 325–340. Springer (2014)
Lammich P (2016) Refinement based verification of imperative data structures. In: Avigad J, Chlipala A (eds) 5th ACM SIGPLAN conference on certified programs and proofs. ACM, pp 27–36
Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) Automated deduction– CADE-26. Lecture notes in computer science, vol. 10395, pp. 237–254. Springer (2017)
Lammich, P.: Refinement to imperative HOL. J Autom Reason 62(4), 481–503 (2019)
Lochbihler, A., Bulwahn, L.: Animating the formalised semantics of a Java-like language. In: van Eekelen Marko, C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Second international conference interactive theorem proving ITP 2011. Lecture notes in computer science, vol. 6898, pp. 216–232. Springer (2011)
Leroy, X.: A formally verified compiler back-end. J Autom Reason 43, 363–446 (2009)
Li, W., Passmore, G.O., Paulson, L.C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. J Autom Reason 62(1), 69–91 (2019)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1–2), 134–152 (1997)
Lammich, P., Sefidgar, S.R.: Formalizing network flow algorithms: a refinement approach in isabelle/hol. J Autom Reason 62(2), 261–280 (2019)
Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft's algorithm. In: Beringer, L., Felty, A.P. (eds.) Third international conference interactive theorem proving ITP, 2012. Lecture notes in computer science, vol. 7406, pp. 166–182. Springer (2012)
Milner, R.: The use of machines to assist in rigorous proof. In: Hoare, C.A.R., Shepherdson, J.C. (eds.) Mathematical logic and programming languages, pp. 77–88. Prentice-Hall (1985)
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J Log Comput 1(4), 497–536 (1991)
The Mizar Mathematical Library. http://mizar.org
Martin-Löf, P.: Constructive mathematics and computer programming. Philos Trans R Soc Ser A 312(1522), 501–518 (1984)
Matichuk, D., Murray, T.C., Wenzel, M.: Eisbach: a proof method language for Isabelle. J Autom Reason 56(3), (2016)
Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: first prototype. Inf Comput 204(10), 1575–1596 (2006)
Matthews D, Wenzel M (2010) Efficient parallel programming in Poly/ML and Isabelle/ML. In: ACM SIGPLAN workshop on declarative aspects of multicore programming (DAMP 2010)
Nipkow T (1991) Higher-order critical pairs. In: Proceedings 6th IEEE symposium logic in computer science. IEEE Press, pp 342–349
Nipkow, T.: Higher-order unification, polymorphism, and subsorts. In: Kaplan, S., Okada, M. (eds.) Proceedings 2nd international workshop conditional and typed rewriting systems, vol 516 of LNCS. Springer (1991)
Nipkow T (1993) Functional unification of higher-order patterns. In: Proceedings 8th IEEE symposium logic in computer science, pp 64–74
Nipkow T (1993) Order-sorted polymorphism in Isabelle. In: Huet G, Plotkin G (eds) Logical environments. Cambridge Uiversity Press, pp 164–188
Nipkow T, Klein G (2014) Concrete semantics with Isabelle/HOL. Springer, 298 pp. http://concrete-semantics.org
Nagele, J., Middeldorp, A.: Certification of classical confluence results for left-linear term rewrite systems. In: Blanchette, J.C., Merz, S. (eds.) 7th international conference interactive theorem proving ITP, 2016. Lecture notes in computer science, vol. 9807, pp. 290–306. Springer (2016)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J ACM 27(2), 356–364 (1980)
Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) Automated deduction–CADE-11, vol 607 of LNCS, pp. 673–676. Springer (1992)
Nipkow, T., Prehofer, C.: Type checking type classes. Principles of programming languages, POPL '93, pp. 409–418. New York, NY, USA. ACM (1993)
Nipkow T, Prehofer C (1998) Higher-order rewriting and equational reasoning. In: Bibel W, Schmitt P (eds) Automated deduction—a basis for applications. Volume I: foundations, vol 8 of Applied logic series. Kluwer, pp 399–430
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher-order logic. Springer, Online at http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf
Nipkow, T., Snelting, G.: Type classes and overloading resolution via order-sorted unification. In: Hughes, J. (ed.) Proceedings 5th ACM conference functional programming languages and computer architecture, vol 523 of LNCS, pp. 1–14. Springer (1991)
Obua, S.: Checking conservativity of overloaded definitions in higher-order logic. In: Pfenning, F. (ed.) Term rewriting and applications, vol 4098 of LNCS, pp. 212–226. Springer (2006)
O'Donnell MJ (1977) Computing in systems described by equations, vol 58 of LNCS. Springer
Overbeek, R.: An implementation of hyper-resolution. Comput Math Appl 1, 201–214 (1975)
Owre S (2006) Random testing in PVS. In: Workshop on automated formal methods (AFM). http://fm.csl.sri.com/AFM06/papers/5-Owre.pdf
Paulson, L.C.: Natural deduction as higher-order resolution. J Log Program 3, 237–258 (1986)
Paulson, L.C.: The foundation of a generic theorem prover. J Autom Reson 5(3), 363–397 (1989)
Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and computer science, pp. 361–386. Academic Press (1990)
Paulson LC (1993) Isabelle's object-logics. Technical report 286, Cambridge University Computer Laboratory
Paulson LC (1994) Isabelle—a generic theorem prover (with contributions by T. Nipkow), vol 828 of Lecture notes in computer science. Springer
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J Comput Secur 6(1–2), 85–128 (1998)
Paulson, L.C.: A generic tableau prover and its integration with Isabelle. J Univers Comput Sci 5(3), 73–87 (1999)
Paulson LC (2003) The relative consistency of the axiom of choice—mechanized using Isabelle/ZF. LMS J Comput Math 6:198–248. http://www.lms.ac.uk/jcm/6/lms2003-001/
Paulson, L.C.: Organizing numerical theories using axiomatic type classes. J Autom Reason 33(1), 29–49 (2004)
Paulson, L.C.: Computational logic: its origins and applications. Proc R Soc Lond A Math Phys Eng Sci 474(2210), (2018)
Peled, D.A.: Combining partial order reductions with on-the-fly model-checking. Form Methods Syst Des 8(1), 39–64 (1996)
Paulson, L.C., Grabczewski, K.: Mechanizing set theory: cardinal arithmetic and the axiom of choice. J Autom Reason 17(3), 291–323 (1996)
Paraskevopoulou, Z., Hritcu, C., Dénès, M., Lampropoulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) Interactive theorem proving, vol 9236 of LNCS, pp. 325–343. Springer (2015)
Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem proving in higher order logics: TPHOLs 2007, LNCS 4732, pp. 232–245. Springer (2007)
Rajan SP (1993) Executing HOL specifications: towards an evaluation semantics for classical higher order logic. In: Claesen Luc JM, Gordon Michael JC (eds) Higher order logic theorem proving and its applications, vol A-20 of IFIP transactions. North-Holland/Elsevier, pp 527–536
Runciman C, Naylor M, Lindblad F (2008) SmallCheck and lazy SmallCheck: automatic exhaustive testing for small values. In: Gill A (ed) Proceediong of the 1st ACM SIGPLAN symposium on Haskell. ACM, pp 37–48
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J ACM 12, 23–41 (1965)
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun 15(2), 91–110 (2002)
Schulz S (2004) System description: E 0.81. In: Basin D, Rusinowitch M (eds) Automated reasoning—second international joint conference, IJCAR 2004, LNAI 3097. Springer, pp 223–228
Shankar, N.: Little engines of proof. In: Eriksson, L.-H., Lindsay, P. (eds.) FME 2002: formal methods–getting IT right: international symposium of formal methods Europe, LNCS 2391, pp. 1–20. Springer (2002)
Siegel, S.F.: What's wrong with on-the-fly partial order reduction. In: Dillig, I., Tasiran, S. (eds.) Computer aided verification (CAV 2019). Springer, LNCS (2019)
Spiridonov A, Khurshid S (2007) Automatic generation of counterexamples for ACL2 using alloy. In: Seventh international workshop on the ACL2 theorem prover and its applications
Slind K, Norrish M (2008) A brief overview of HOL4. In: Mohamed O, Muñoz C, Tahar S (eds) Theorem proving in higher order logics, TPHOLs 2008, pp 28–32
Sumners R (2002) Checking ACL2 theorems via SAT checking. In: Third international workshop on the ACL2 theorem prover and its applications
Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) Tools and algorithms for the construction and analysis of systems, vol 4424 of LNCS, pp. 632–647. Springer (2007)
Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) 22nd international conference theorem proving in higher order logics, TPHOLs 2009. Lecture notes in computer science, vol. 5674, pp. 452–468. Springer (2009)
Weber, T.: Bounded model generation for Isabelle/HOL. In: Ahrendt, W., Baumgartner, P., de Nivelle, H., Ranise, S., Tinelli, C. (eds.) Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), vol 125(3) of Electronic notes in theoretical computer science, pp. 103–116. Elsevier (2005)
Weber T (2008) SAT-based finite model generation for higher-order logic. PhD thesis, Technical University Munich, Germany
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of automated reasoning, vol II, chapter 27, pp 1965–2013. Elsevier Science (2001)
Wenzel Ma (1997) Type classes and overloading in higher-order logic. In: Theorem proving in higher order logics, vol 1275 of LNCS. Springer, pp 307–322
Wenzel M (2007) Isabelle/Isar—a generic framework for human-readable proof documents. Stud Log Gramm Rhetor 10(23):277–297 From Insight to Proof—Festschrift in Honour of Andrzej Trybulec
Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., et al. (eds.) Conference on intelligent computer mathematics (CICM 2011), vol 6824 of LNAI. Springer (2011)
Wenzel M (2013) READ-EVAL-PRINT in parallel and asynchronous proof-checking. In: Kaliszyk C, Lüth C (eds) User interfaces for theorem provers (UITP 2012), vol 118 of Electronic proceedings in theoretical computer science
Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive theorem proving (ITP 2013). Lecture notes in computer science, vol. 7998. Springer (2013)
Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) Interactive theorem proving (ITP 2014), vol 8558 of LNCS. Springer (2014)
Wenzel M (2019) Interaction with formal mathematical documents in Isabelle/PIDE. In: Kaliszyk C, Brady E, Kohlhase A, Sacerdoti CC (eds) Intelligent computer mathematics (CICM 2019), vol 11617 of LNAI. Springer. https://arxiv.org/abs/1905.01735
Wiedijk, F.: Mizar light for HOL light. In: Boulton, R.J., Jackson, P.B. (eds.) Theorem proving in higher order logics, TPHOLs 2001, Berlin, Heidelberg, pp. 378–393. Springer, Berlin (2001)
Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) Tools and algorithms for the construction and analysis of systems, TACAS 2018. Lecture notes in computer science, vol. 10805, pp. 61–78. Springer (2018)
Wood C (2018) The strange numbers that birthed modern algebra. https://www.quantamagazine.org/the-strange-numbers-that-birthed-modern-algebra-20180906/
Acknowledgements
We thank the referees, Jasmin Blanchette, Michael Norrish and Andrei Popescu for valuable comments on drafts of this paper. The work reported above was funded by the British EPSRC, the German DFG and various European Union funding agencies.
Author information
Authors and Affiliations
Corresponding author
Additional information
Cliff Jones and José N. Oliveira
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
Paulson, L.C., Nipkow, T. & Wenzel, M. From LCF to Isabelle/HOL. Form Asp Comp 31, 675–698 (2019). https://doi.org/10.1007/s00165-019-00492-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-019-00492-1