{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:14Z","timestamp":1740123374522,"version":"3.37.3"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,5,11]],"date-time":"2018-05-11T00:00:00Z","timestamp":1525996800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-018-9465-5","type":"journal-article","created":{"date-parts":[[2018,5,11]],"date-time":"2018-05-11T05:49:07Z","timestamp":1526017747000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Introduction to Milestones in Interactive Theorem Proving"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1275-315X","authenticated-orcid":false,"given":"Jeremy","family":"Avigad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregor","family":"Snelting","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,11]]},"reference":[{"key":"9465_CR1","doi-asserted-by":"crossref","unstructured":"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\u20139, 2008. Proceedings, vol. 5295 of Lecture Notes in Computer Science, pp. 209\u2013224. Springer, New York (2008)","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"9465_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"9465_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013May 4, 2003, Revised Selected Papers, vol. 3085 of Lecture Notes in Computer Science, pp. 34\u201350. Springer (2003)","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"9465_CR4","doi-asserted-by":"crossref","unstructured":"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\u201312, 2000, Selected Papers, vol. 1869 of Lecture Notes in Computer Science, pp. 24\u201340. Springer (2000)","DOI":"10.1007\/3-540-45842-5_2"},{"key":"9465_CR5","doi-asserted-by":"crossref","unstructured":"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\u201314, 2010. Proceedings, vol. 6172 of Lecture Notes in Computer Science, pp. 131\u2013146. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"9465_CR6","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16\u201319, 2010. Proceedings, vol. 6173 of Lecture Notes in Computer Science, pp. 107\u2013121. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"9465_CR7","unstructured":"Hupel, L., Nipkow, T.: A verified compiler from Isabelle\/HOL to CakeML. In: Ahmed, A. (ed.) Programming Languages and Systems\u201327th 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\u201320 (2018)"},{"key":"9465_CR8","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales\u2014A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u201999, Nice, France, September, 1999, Proceedings, vol. 1690 of Lecture Notes in Computer Science, pp. 149\u2013166. Springer (1999)","DOI":"10.1007\/3-540-48256-3_11"},{"key":"9465_CR9","unstructured":"Klein, G.: Verified Java bytecode verification. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, Germany (2003)"},{"issue":"6","key":"9465_CR10","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"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\u2013115 (2010)","journal-title":"Commun. ACM"},{"issue":"4","key":"9465_CR11","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"9465_CR12","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF00297246","volume":"4","author":"U Martin","year":"1988","unstructured":"Martin, U., Nipkow, T.: Unification in Boolean rings. J. Autom. Reason. 4(4), 381\u2013396 (1988)","journal-title":"J. Autom. Reason."},{"issue":"3\/4","key":"9465_CR13","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0747-7171(89)80013-6","volume":"7","author":"U Martin","year":"1989","unstructured":"Martin, U., Nipkow, T.: Boolean unification\u2013the story so far. J. Symb. Comput. 7(3\/4), 275\u2013293 (1989)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"9465_CR14","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497\u2013536 (1991)","journal-title":"J. Log. Comput."},{"key":"9465_CR15","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0167-6423(89)90038-5","volume":"12","author":"T Nipkow","year":"1989","unstructured":"Nipkow, T.: Equational reasoning in Isabelle. Sci. Comput. Program. 12, 123\u2013149 (1989)","journal-title":"Sci. Comput. Program."},{"key":"9465_CR16","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/BF01887212","volume":"1","author":"T Nipkow","year":"1989","unstructured":"Nipkow, T.: Term rewriting and beyond\u2013theorem proving in Isabelle. Form. Asp. Comput. 1, 320\u2013338 (1989)","journal-title":"Form. Asp. Comput."},{"issue":"4","key":"9465_CR17","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1145\/96559.96569","volume":"37","author":"T Nipkow","year":"1990","unstructured":"Nipkow, T.: Unification in primal algebras, their powers and their varieties. J. ACM 37(4), 742\u2013776 (1990)","journal-title":"J. ACM"},{"key":"9465_CR18","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1093\/comjnl\/34.1.34","volume":"34","author":"T Nipkow","year":"1991","unstructured":"Nipkow, T.: Constructive rewriting. Comput. J. 34, 34\u201341 (1991)","journal-title":"Comput. J."},{"key":"9465_CR19","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991), Amsterdam, The Netherlands, July 15\u201318 (1991)"},{"key":"9465_CR20","doi-asserted-by":"crossref","unstructured":"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\u2013447 (1991)","DOI":"10.1007\/3-540-54317-1_112"},{"key":"9465_CR21","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Functional unification of higher-order patterns. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS \u201993), Montreal, Canada, June 19\u201323, 1993, pp. 64\u201374. IEEE Computer Society (1993)","DOI":"10.1109\/LICS.1993.287599"},{"key":"9465_CR22","first-page":"164","volume-title":"Logical Environments","author":"T Nipkow","year":"1993","unstructured":"Nipkow, T.: Order-sorted polymorphism in Isabelle. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 164\u2013188. Cambridge University Press, Cambridge (1993)"},{"issue":"2","key":"9465_CR23","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Form. Asp. Comput. 10(2), 171\u2013186 (1998)","journal-title":"Form. Asp. Comput."},{"key":"9465_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Invited talk: Embedding programming languages in theorem provers (abstract). In: Ganzinger, H. (ed.) Automated Deduction\u2014CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7\u201310, 1999, Proceedings, vol. 1632 of Lecture Notes in Computer Science, pp. 398. Springer (1999)","DOI":"10.1007\/3-540-48660-7_38"},{"key":"9465_CR25","doi-asserted-by":"crossref","unstructured":"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\u20136, 2001, Proceedings, vol. 2030 of Lecture Notes in Computer Science, pp. 347\u2013363. Springer (2001)","DOI":"10.1007\/3-540-45315-6_23"},{"key":"9465_CR26","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-39185-1_15","volume-title":"Types for Proofs and Programs","author":"T Nipkow","year":"2003","unstructured":"Nipkow, T.: Structured proofs in Isar\/HOL. In: Geuvers, H., Wiedijk, F. (eds.) Types for Proofs and Programs, pp. 259\u2013278. Springer, Berlin (2003)"},{"issue":"2","key":"9465_CR27","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T Nipkow","year":"2010","unstructured":"Nipkow, T.: Linear quantifier elimination. J. Autom. Reason. 45(2), 189\u2013212 (2010)","journal-title":"J. Autom. Reason."},{"key":"9465_CR28","doi-asserted-by":"crossref","unstructured":"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\u201320, 2006, Proceedings, vol. 4130 of Lecture Notes in Computer Science, pp. 21\u201335. Springer (2006)","DOI":"10.1007\/11814771_4"},{"key":"9465_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics-With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics-With Isabelle\/HOL. Springer, New York (2014)"},{"key":"9465_CR30","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C.: Isabelle-91 (system abstract). In: Kapur, D. (ed.) Automated Deduction\u2014CADE-11 International Conference, LNAI 607, pp. 673\u2013676. Springer (1992)","DOI":"10.1007\/3-540-55602-8_201"},{"key":"9465_CR31","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Prehofer, C.: Type checking type classes. In: Principles of Programming Languages, POPL \u201993, pp. 409\u2013418. ACM, New York (1993)","DOI":"10.1145\/158511.158698"},{"key":"9465_CR32","doi-asserted-by":"crossref","unstructured":"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\u201312, 1991, Proceedings, vol. 488 of Lecture Notes in Computer Science, pp. 200\u2013214. Springer (1991)","DOI":"10.1007\/3-540-53904-2_97"},{"key":"9465_CR33","unstructured":"Nipkow, T., Slind, K.: I\/O automata in Isabelle\/HOL. In: Dybjer, P., Nordstr\u00f6m, B., Smith, J. (eds.) Types for Proofs and Programs: International Workshop TYPES \u201994 B\u00e5stad, Sweden, June 6\u201310, 1994 Selected Papers, pp. 101\u2013119. Springer (1995)"},{"key":"9465_CR34","doi-asserted-by":"crossref","unstructured":"Nipkow, T., von Oheimb, D.: $$\\text{Java}_{{\\ell } ight}$$ Java \u2113 i g h t is type-safe\u2014definitely. In: Principles of Programming Languages, POPL \u201998, pp. 161\u2013170. ACM (1998)","DOI":"10.1145\/268946.268960"},{"key":"9465_CR35","unstructured":"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\u20137, 1983, Proceedings, vol. 145 of Lecture Notes in Computer Science, pp. 257\u2013268. Springer (1983)"},{"key":"9465_CR36","doi-asserted-by":"crossref","unstructured":"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\u201318, 2005, Proceedings, vol. 3452 of Lecture Notes in Computer Science, pp. 398\u2013414. Springer (2004)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9465_CR37","unstructured":"von Oheimb, D.: Analyzing Java in Isabelle\/HOL: formalization, type safety and Hoare logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, Germany (2001)"},{"key":"9465_CR38","unstructured":"Wenzel, M.: Isabelle\/jEdit\u2014a 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\u201411th 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\u201313, 2012. Proceedings, vol. 7362 of Lecture Notes in Computer Science, pp. 468\u2013471. Springer (2012)"},{"key":"9465_CR39","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a versatile environment for human-readable formal proof documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9465-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9465-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9465-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T15:20:54Z","timestamp":1693668054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9465-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,11]]},"references-count":39,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9465"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9465-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,5,11]]},"assertion":[{"value":"25 April 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 April 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 May 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}