Introduction to “Milestones in interactive theorem proving”. (English) Zbl 1398.00118


00B30 Festschriften
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Biographic References:

Nipkow, Tobias
Full Text: DOI Link


[1] Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N., Starostin, A.: The Verisoft approach to systems verification. In: Shankar, N., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, vol. 5295 of Lecture Notes in Computer Science, pp. 209-224. Springer, New York (2008)
[2] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098
[3] Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30-May 4, 2003, Revised Selected Papers, vol. 3085 of Lecture Notes in Computer Science, pp. 34-50. Springer (2003) · Zbl 1100.68615
[4] Berghofer, S., Nipkow, T.: Executing Higher Order Logic. In: Aagaard, M., Harrison, J. (eds.) Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, vol. 1869 of Lecture Notes in Computer Science, pp. 24-40. Springer (2000) · Zbl 1054.68133
[5] Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, vol. 6172 of Lecture Notes in Computer Science, pp. 131-146. Springer (2010) · Zbl 1291.68326
[6] Böhme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., Hähnle, R. (eds.) Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, vol. 6173 of Lecture Notes in Computer Science, pp. 107-121. Springer (2010) · Zbl 1291.68327
[7] Hupel, L., Nipkow, T.: A verified compiler from Isabelle/HOL to CakeML. In: Ahmed, A. (ed.) Programming Languages and Systems-27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20 (2018)
[8] Kammüller, F., Wenzel, M., Paulson, L.C.: Locales—A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings, vol. 1690 of Lecture Notes in Computer Science, pp. 149-166. Springer (1999)
[9] Klein, G.: Verified Java bytecode verification. PhD thesis, Technische Universität München, Germany (2003)
[10] 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, 107-115, (2010)
[11] Klein, G; Nipkow, T, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Trans. Program. Lang. Syst., 28, 619-695, (2006)
[12] Martin, U; Nipkow, T, Unification in Boolean rings, J. Autom. Reason., 4, 381-396, (1988) · Zbl 0659.68111
[13] Martin, U; Nipkow, T, Boolean unification-the story so far, J. Symb. Comput., 7, 275-293, (1989) · Zbl 0682.68093
[14] Miller, D, A logic programming language with lambda-abstraction, function variables, and simple unification, J. Log. Comput., 1, 497-536, (1991) · Zbl 0738.68016
[15] Nipkow, T, Equational reasoning in isabelle, Sci. Comput. Program., 12, 123-149, (1989) · Zbl 0683.68081
[16] Nipkow, T, Term rewriting and beyond-theorem proving in isabelle, Form. Asp. Comput., 1, 320-338, (1989) · Zbl 0694.68059
[17] Nipkow, T, Unification in primal algebras, their powers and their varieties, J. ACM, 37, 742-776, (1990) · Zbl 0711.68092
[18] Nipkow, T, Constructive rewriting, Comput. J., 34, 34-41, (1991)
[19] Nipkow, T.: Higher-order critical pairs. In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS ’91), Amsterdam, The Netherlands, July 15-18 (1991)
[20] Nipkow, T.: Higher-order unification, polymorphism, and subsorts. In: Kaplan, S., Okada, M. (eds.) Conditional and Typed Rewriting Systems. CTRS 1990, vol. 516, pp. 436-447 (1991)
[21] Nipkow, T.: Functional unification of higher-order patterns. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS ’93), Montreal, Canada, June 19-23, 1993, pp. 64-74. IEEE Computer Society (1993)
[22] Nipkow, T; Huet, G (ed.); Plotkin, G (ed.), Order-sorted polymorphism in isabelle, 164-188, (1993), Cambridge
[23] Nipkow, T, Winskel is (almost) right: towards a mechanized semantics textbook, Form. Asp. Comput., 10, 171-186, (1998) · Zbl 0910.68138
[24] Nipkow, T.: Invited talk: Embedding programming languages in theorem provers (abstract). In: Ganzinger, H. (ed.) Automated Deduction—CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, vol. 1632 of Lecture Notes in Computer Science, pp. 398. Springer (1999) · Zbl 0694.68059
[25] Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, vol. 2030 of Lecture Notes in Computer Science, pp. 347-363. Springer (2001) · Zbl 0978.68512
[26] Nipkow, T; Geuvers, H (ed.); Wiedijk, F (ed.), Structured proofs in isar/HOL, 259-278, (2003), Berlin · Zbl 1023.68657
[27] Nipkow, T, Linear quantifier elimination, J. Autom. Reason., 45, 189-212, (2010) · Zbl 1207.68339
[28] Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: tame graphs. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, vol. 4130 of Lecture Notes in Computer Science, pp. 21-35. Springer (2006) · Zbl 1222.52018
[29] Nipkow, T., Klein, G.: Concrete Semantics-With Isabelle/HOL. Springer, New York (2014) · Zbl 1410.68004
[30] Nipkow, T., Paulson, L.C.: Isabelle-91 (system abstract). In: Kapur, D. (ed.) Automated Deduction—CADE-11 International Conference, LNAI 607, pp. 673-676. Springer (1992)
[31] Nipkow, T., Prehofer, C.: Type checking type classes. In: Principles of Programming Languages, POPL ’93, pp. 409-418. ACM, New York (1993)
[32] Nipkow, T., Qian, Z.: Modular higher-order \(E\)-unification. In: Book, R.V. (ed.) Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, vol. 488 of Lecture Notes in Computer Science, pp. 200-214. Springer (1991)
[33] Nipkow, T., Slind, K.: I/O automata in Isabelle/HOL. In: Dybjer, P., Nordström, B., Smith, J. (eds.) Types for Proofs and Programs: International Workshop TYPES ’94 Båstad, Sweden, June 6-10, 1994 Selected Papers, pp. 101-119. Springer (1995)
[34] Nipkow, T., von Oheimb, D.: \(\text{Java}_{{ℓ } ight}\) is type-safe—definitely. In: Principles of Programming Languages, POPL ’98, pp. 161-170. ACM (1998)
[35] Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) Theoretical Computer Science, 6th GI-Conference, Dortmund, Germany, January 5-7, 1983, Proceedings, vol. 145 of Lecture Notes in Computer Science, pp. 257-268. Springer (1983) · Zbl 0493.68024
[36] Schirmer, N.: A verification environment for sequential imperative programs in Isabelle/HOL. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, vol. 3452 of Lecture Notes in Computer Science, pp. 398-414. Springer (2004) · Zbl 1108.68410
[37] von Oheimb, D.: Analyzing Java in Isabelle/HOL: formalization, type safety and Hoare logic. PhD thesis, Technische Universität München, Germany (2001) · Zbl 0997.68019
[38] Wenzel, M.: Isabelle/jEdit—a prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Reis, G.D., Sojka, P., Wenzel, M., Sorge, V. (eds.) Intelligent Computer Mathematics—11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, vol. 7362 of Lecture Notes in Computer Science, pp. 468-471. Springer (2012) · Zbl 1245.68013
[39] Wenzel, M.: Isabelle/Isar—a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, Technische Universität München (2002)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.