| [1] |
Antoy, S.; Hanus, M., Functional logic programming, Commun ACM, 53, 4, 74-85 (2010) · doi:10.1145/1721654.1721675 |
| [2] |
Arthan, R., On definitions of constants and types in HOL, J Autom Reason, 56, 3, 205-219 (2016) · Zbl 1356.68173 · doi:10.1007/s10817-016-9366-4 |
| [3] |
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 · Zbl 0971.68627 |
| [4] |
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 · Zbl 1188.68258 |
| [5] |
Ballarin, C., Locales: a module system for mathematical theories, J Autom Reason, 52, 2, 123-153 (2014) · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7 |
| [6] |
Barwise J (1977) An introduction to first-order logic. In: Barwise J (ed) Handbook of mathematical logic. North-Holland, pp 5-46 |
| [7] |
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) · Zbl 1433.68530 · doi:10.1007/s10817-017-9440-6 |
| [8] |
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 · Zbl 1252.68249 |
| [9] |
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 · Zbl 1348.68214 |
| [10] |
Blanchette, Jc; Böhme, S.; Paulson, Lc, Extending Sledgehammer with SMT solvers, J Autom Reason, 51, 1, 109-128 (2013) · Zbl 1314.68272 · doi:10.1007/s10817-013-9278-5 |
| [11] |
Bertot Y, Castéran P (2004) Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer · Zbl 1069.68095 |
| [12] |
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 · Zbl 1165.68352 |
| [13] |
Brunner, J.; Lammich, P., Formal verification of an executable LTL model checker with partial order reduction, J Autom Reason, 60, 1, 3-21 (2018) · Zbl 1426.68162 · doi:10.1007/s10817-017-9418-4 |
| [14] |
Blanchette JC (2012) Automatic proofs and refutations for higher-order logic. PhD thesis, Technical University Munich |
| [15] |
Blanchette, Jc, Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions, Softw Qual J, 21, 1, 101-126 (2013) · doi:10.1007/s11219-011-9148-5 |
| [16] |
Boyer RS, Moore JS (1979) A computational logic. Academic Press · Zbl 0448.68020 |
| [17] |
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 · Zbl 1054.68133 |
| [18] |
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 |
| [19] |
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 · Zbl 1291.68326 |
| [20] |
Bulwahn L (2012) Counterexample generation for higher-order logic using functional and logic programming. PhD thesis, Technical University Munich · Zbl 1352.68039 |
| [21] |
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 · Zbl 1383.68071 |
| [22] |
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 · Zbl 1352.68039 |
| [23] |
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 · Zbl 1490.68018 |
| [24] |
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 |
| [25] |
Clocksin WF, Mellish CS (1987) Programming in prolog, 3rd edn. Springer · Zbl 0613.68010 |
| [26] |
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 |
| [27] |
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 |
| [28] |
Divasón, J.; Joosten, Sjc; Thiemann, R.; Yamada, A., A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2019), J Autom Reason: Published online, J Autom Reason |
| [29] |
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 · Zbl 1133.68009 |
| [30] |
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) · Zbl 1465.68279 |
| [31] |
Debray, Sk; Warren, Ds, Automatic mode inference for logic programs, J Log Program, 5, 3, 207-229 (1988) · Zbl 0647.68010 · doi:10.1016/0743-1066(88)90010-6 |
| [32] |
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 |
| [33] |
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) |
| [34] |
Futatsugi, K.; Goguen, Ja; Jouannaud, J-P; Meseguer, J., Principles of OBJ2, 12th ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL), 52-66 (1985), USA. ACM: New York, NY, USA. ACM |
| [35] |
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) · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y |
| [36] |
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) |
| [37] |
Gomes, Victor B. F.; Kleppmann, Martin; Mulligan, Dominic P.; Beresford, Alastair R., Verifying strong eventual consistency in distributed systems, Proceedings of the ACM on Programming Languages, 1, OOPSLA, 1-28 (2017) · doi:10.1145/3133933 |
| [38] |
Grabowski, A.; Korniłowicz, A.; Naumowicz, A., Four decades of Mizar, J Autom Reason, 55, 3, 191-198 (2015) · Zbl 1336.00111 · doi:10.1007/s10817-015-9345-1 |
| [39] |
Gordon MJC, Melham TF (eds) (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press · Zbl 0779.68007 |
| [40] |
Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J Formaliz Reason 3(2), (2010) · Zbl 1211.68368 |
| [41] |
Gordon MJC, Milner R, Wadsworth CP (1979) Edinburgh LCF: a mechanised logic of computation. LNCS 78. Springer · Zbl 0421.68039 |
| [42] |
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) · Zbl 0456.68011 |
| [43] |
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) · Zbl 0612.94015 |
| [44] |
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) |
| [45] |
Gordon, M. J. C., Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 373, 2039, 20140234 (2015) · Zbl 1353.68250 · doi:10.1098/rsta.2014.0234 |
| [46] |
Hales, T.; Adams, M.; Bauer, G.; Dang, Td; Harrison, J.; Hoang, Lt; Kaliszyk, C.; Magron, V.; Mclaughlin, S.; Nguyen, Tt, A formal proof of the Kepler conjecture, Forum Math Pi, 5, e2 (2017) · Zbl 1379.52018 · doi:10.1017/fmp.2017.1 |
| [47] |
Haftmann F (2009) Code generation from specifications in higher order logic. PhD thesis, Technische Universität München |
| [48] |
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) |
| [49] |
Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, J ACM, 40, 1, 143-184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060 |
| [50] |
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) · Zbl 1317.68213 |
| [51] |
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) · Zbl 1317.68212 |
| [52] |
Hunt, Warren A.; Kaufmann, Matt; Moore, J. Strother; Slobodova, Anna, Industrial hardware and software verification with ACL2, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375, 2104, 20150399 (2017) · doi:10.1098/rsta.2015.0399 |
| [53] |
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) · Zbl 1284.68131 |
| [54] |
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) · Zbl 1418.68045 |
| [55] |
Hoffmann Christoph, M.; O’Donnell Michael, J., Programming with equations, ACM Trans Program Lang Syst, 4, 1, 83-112 (1982) · Zbl 0481.68008 · doi:10.1145/357153.357158 |
| [56] |
Holzmann, Gj, The model checker SPIN, IEEE Trans Softw Eng, 23, 5, 279-295 (1997) · doi:10.1109/32.588521 |
| [57] |
Huet, Gp, A unification algorithm for typed \(\lambda \)-calculus, Theor Comput Sci, 1, 27-57 (1975) · Zbl 0337.68027 · doi:10.1016/0304-3975(75)90011-0 |
| [58] |
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) · Zbl 1178.68529 |
| [59] |
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) · Zbl 1246.68197 |
| [60] |
Jackson D (2006) Software abstractions. Logic, language, and analysis. MIT Press |
| [61] |
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) · doi:10.1145/1743546.1743574 |
| [62] |
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 |
| [63] |
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 · Zbl 1284.68405 |
| [64] |
Kunčar, Ondřej; Popescu, Andrei, Safety and conservativity of definitions in HOL and Isabelle/HOL, Proceedings of the ACM on Programming Languages, 2, POPL, 1-26 (2017) · doi:10.1145/3158112 |
| [65] |
Kunčar, O.; Popescu, A., A consistent foundation for Isabelle/HOL, J. Autom Reason, 62, 4, 531-555 (2019) · Zbl 1465.68289 · doi:10.1007/s10817-018-9454-8 |
| [66] |
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) |
| [67] |
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) · Zbl 1317.68216 |
| [68] |
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) · Zbl 1416.68168 |
| [69] |
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 |
| [70] |
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) · Zbl 1468.68133 |
| [71] |
Lammich, P., Refinement to imperative HOL, J Autom Reason, 62, 4, 481-503 (2019) · Zbl 1465.68291 · doi:10.1007/s10817-017-9437-1 |
| [72] |
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) · Zbl 1342.68294 |
| [73] |
Leroy, X., A formally verified compiler back-end, J Autom Reason, 43, 363-446 (2009) · Zbl 1185.68215 · doi:10.1007/s10817-009-9155-4 |
| [74] |
Li, W.; Passmore, Go; Paulson, Lc, Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL, J Autom Reason, 62, 1, 69-91 (2019) · Zbl 1468.68298 · doi:10.1007/s10817-017-9424-6 |
| [75] |
Larsen, Kg; Pettersson, P.; Yi, W., UPPAAL in a nutshell. STTT, 1, 1-2, 134-152 (1997) · Zbl 1060.68577 · doi:10.1007/s100090050010 |
| [76] |
Lammich, P.; Sefidgar, Sr, Formalizing network flow algorithms: a refinement approach in isabelle/hol, J Autom Reason, 62, 2, 261-280 (2019) · Zbl 1468.68328 · doi:10.1007/s10817-017-9442-4 |
| [77] |
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) · Zbl 1360.68757 |
| [78] |
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) |
| [79] |
Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification, J Log Comput, 1, 4, 497-536 (1991) · Zbl 0738.68016 · doi:10.1093/logcom/1.4.497 |
| [80] |
The Mizar Mathematical Library. http://mizar.org · Zbl 1278.68290 |
| [81] |
Martin-Löf, P., Constructive mathematics and computer programming, Philos Trans R Soc Ser A, 312, 1522, 501-518 (1984) · Zbl 0552.03040 · doi:10.1098/rsta.1984.0073 |
| [82] |
Matichuk, Daniel; Murray, Toby; Wenzel, Makarius, Eisbach: A Proof Method Language for Isabelle, Journal of Automated Reasoning, 56, 3, 261-282 (2016) · Zbl 1356.68195 · doi:10.1007/s10817-015-9360-2 |
| [83] |
Meng, J.; Quigley, C.; Paulson, Lc, Automation for interactive proof: first prototype, Inf Comput, 204, 10, 1575-1596 (2006) · Zbl 1103.68113 · doi:10.1016/j.ic.2005.05.010 |
| [84] |
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) |
| [85] |
Nipkow T (1991) Higher-order critical pairs. In: Proceedings 6th IEEE symposium logic in computer science. IEEE Press, pp 342-349 |
| [86] |
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) · Zbl 1507.68075 |
| [87] |
Nipkow T (1993) Functional unification of higher-order patterns. In: Proceedings 8th IEEE symposium logic in computer science, pp 64-74 |
| [88] |
Nipkow T (1993) Order-sorted polymorphism in Isabelle. In: Huet G, Plotkin G (eds) Logical environments. Cambridge Uiversity Press, pp 164-188 |
| [89] |
Nipkow T, Klein G (2014) Concrete semantics with Isabelle/HOL. Springer, 298 pp. http://concrete-semantics.org · Zbl 1410.68004 |
| [90] |
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) · Zbl 1478.68117 |
| [91] |
Nelson, G.; Oppen, Dc, Fast decision procedures based on congruence closure, J ACM, 27, 2, 356-364 (1980) · Zbl 0441.68111 · doi:10.1145/322186.322198 |
| [92] |
Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) Automated deduction-CADE-11, vol 607 of LNCS, pp. 673-676. Springer (1992) |
| [93] |
Nipkow, T.; Prehofer, C., Type checking type classes, Principles of programming languages, POPL ’93, 409-418 (1993), USA. ACM: New York, NY, USA. ACM |
| [94] |
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 · Zbl 0970.68081 |
| [95] |
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 · Zbl 0994.68131 |
| [96] |
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) |
| [97] |
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) · Zbl 1151.68637 |
| [98] |
O’Donnell MJ (1977) Computing in systems described by equations, vol 58 of LNCS. Springer · Zbl 0421.68038 |
| [99] |
Overbeek, R., An implementation of hyper-resolution, Comput Math Appl, 1, 201-214 (1975) · Zbl 0339.68060 · doi:10.1016/0898-1221(75)90019-X |
| [100] |
Owre S (2006) Random testing in PVS. In: Workshop on automated formal methods (AFM). http://fm.csl.sri.com/AFM06/papers/5-Owre.pdf |
| [101] |
Paulson, Lc, Natural deduction as higher-order resolution, J Log Program, 3, 237-258 (1986) · Zbl 0613.68035 · doi:10.1016/0743-1066(86)90015-4 |
| [102] |
Paulson, Lc, The foundation of a generic theorem prover, J Autom Reson, 5, 3, 363-397 (1989) · Zbl 0679.68173 · doi:10.1007/BF00248324 |
| [103] |
Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and computer science, pp. 361-386. Academic Press (1990) |
| [104] |
Paulson LC (1993) Isabelle’s object-logics. Technical report 286, Cambridge University Computer Laboratory |
| [105] |
Paulson LC (1994) Isabelle—a generic theorem prover (with contributions by T. Nipkow), vol 828 of Lecture notes in computer science. Springer · Zbl 0825.68059 |
| [106] |
Paulson, Lc, The inductive approach to verifying cryptographic protocols, J Comput Secur, 6, 1-2, 85-128 (1998) · doi:10.3233/JCS-1998-61-205 |
| [107] |
Paulson, Lc, A generic tableau prover and its integration with Isabelle, J Univers Comput Sci, 5, 3, 73-87 (1999) · Zbl 0961.68116 |
| [108] |
Paulson, Lawrence C., The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf, LMS Journal of Computation and Mathematics, 6, 198-248 (2003) · Zbl 1053.03009 · doi:10.1112/S1461157000000449 |
| [109] |
Paulson, Lc, Organizing numerical theories using axiomatic type classes, J Autom Reason, 33, 1, 29-49 (2004) · Zbl 1071.68092 · doi:10.1007/s10817-004-3997-6 |
| [110] |
Paulson, Lawrence C., Computational logic: its origins and applications, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, 474, 2210, 20170872 (2018) · Zbl 1402.68160 · doi:10.1098/rspa.2017.0872 |
| [111] |
Peled, Da, Combining partial order reductions with on-the-fly model-checking, Form Methods Syst Des, 8, 1, 39-64 (1996) · Zbl 1425.68267 · doi:10.1007/BF00121262 |
| [112] |
Paulson, Lc; Grabczewski, K., Mechanizing set theory: cardinal arithmetic and the axiom of choice, J Autom Reason, 17, 3, 291-323 (1996) · Zbl 0868.03005 · doi:10.1007/BF00283132 |
| [113] |
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) · Zbl 1465.68050 |
| [114] |
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) · Zbl 1144.68364 |
| [115] |
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 |
| [116] |
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 |
| [117] |
Robinson, Ja, A machine-oriented logic based on the resolution principle, J ACM, 12, 23-41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253 |
| [118] |
Riazanov, A.; Voronkov, A., The design and implementation of VAMPIRE, AI Commun, 15, 2, 91-110 (2002) · Zbl 1021.68082 |
| [119] |
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 · Zbl 1126.68578 |
| [120] |
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) · Zbl 1064.68558 |
| [121] |
Siegel, Sf; Dillig, I.; Tasiran, S., What’s wrong with on-the-fly partial order reduction, Computer aided verification (CAV 2019) (2019), LNCS: Springer, LNCS |
| [122] |
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 |
| [123] |
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 · Zbl 1165.68474 |
| [124] |
Sumners R (2002) Checking ACL2 theorems via SAT checking. In: Third international workshop on the ACL2 theorem prover and its applications |
| [125] |
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) · Zbl 1186.68304 |
| [126] |
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) · Zbl 1252.68265 |
| [127] |
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) · Zbl 1271.68015 |
| [128] |
Weber T (2008) SAT-based finite model generation for higher-order logic. PhD thesis, Technical University Munich, Germany |
| [129] |
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) · Zbl 1011.68129 |
| [130] |
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 |
| [131] |
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 |
| [132] |
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) · Zbl 1335.68239 |
| [133] |
Wenzel, Makarius, READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking, Electronic Proceedings in Theoretical Computer Science, 118, 57-71 (2013) · doi:10.4204/EPTCS.118.4 |
| [134] |
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) · Zbl 1317.68235 |
| [135] |
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) · Zbl 1416.68182 |
| [136] |
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 · Zbl 1428.68347 |
| [137] |
Wiedijk, F.; Boulton, Rj; Jackson, Pb, Mizar light for HOL light, Theorem proving in higher order logics, TPHOLs 2001, Berlin, Heidelberg, 378-393 (2001), Berlin: Springer, Berlin · Zbl 1005.68539 |
| [138] |
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) · Zbl 1423.68294 |
| [139] |
Wood C (2018) The strange numbers that birthed modern algebra. https://www.quantamagazine.org/the-strange-numbers-that-birthed-modern-algebra-20180906/ |
