{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:48:57Z","timestamp":1771573737916,"version":"3.50.1"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T00:00:00Z","timestamp":1453075200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000934","name":"Department of Industry, Innovation, Science, Research and Tertiary Education, Australian Government","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000934","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008242","name":"National ICT Australia","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008242","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s10817-015-9360-2","type":"journal-article","created":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T03:05:56Z","timestamp":1453086356000},"page":"261-282","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Eisbach: A Proof Method Language for Isabelle"],"prefix":"10.1007","volume":"56","author":[{"given":"Daniel","family":"Matichuk","sequence":"first","affiliation":[]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[]},{"given":"Makarius","family":"Wenzel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"9360_CR1","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 (TYPES 2003). Lecture Notes in Computer Science, vol. 3085. Springer (2003). doi: 10.1007\/978-3-540-24849-1_3","DOI":"10.1007\/978-3-540-24849-1_3"},{"issue":"2","key":"9360_CR2","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). doi: 10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"key":"9360_CR3","doi-asserted-by":"crossref","unstructured":"Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Wenzel, M. (ed.) Conferences on Intelligent Computer Mathematics (CICM)\/Mathematical Knowledge Management. Springer (2012). doi: 10.1007\/978-3-642-31374-5_3","DOI":"10.1007\/978-3-642-31374-5_3"},{"issue":"6","key":"9360_CR4","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/1993316.1993526","volume":"46","author":"A Chlipala","year":"2011","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. ACM SIGPLAN Not. 46(6), 234 (2011). doi: 10.1145\/1993316.1993526","journal-title":"ACM SIGPLAN Not."},{"key":"9360_CR5","doi-asserted-by":"crossref","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) 21st TPHOLs, LNCS, vol. 5170, pp. 167\u2013182. Springer, Montreal, Canada (2008). doi: 10.1007\/978-3-540-71067-7_16","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"9360_CR6","doi-asserted-by":"crossref","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: International Conference on Logic for Programming and Artificial Intelligence & Reasoning, LNCS, vol. 1955. Springer (2000). doi: 10.1007\/3-540-44404-1_7","DOI":"10.1007\/3-540-44404-1_7"},{"key":"9360_CR7","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formaliz. Reason. (2010). doi: 10.6092\/issn.1972-5787\/1979"},{"issue":"4","key":"9360_CR8","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1017\/S0956796813000051","volume":"23","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. J. Funct. Program. 23(4), 357\u2013401 (2013). doi: 10.1017\/S0956796813000051","journal-title":"J. Funct. Program."},{"key":"9360_CR9","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanized Logic of Computation. LNCS 78. Springer (1979). doi: 10.1007\/3-540-09724-4","DOI":"10.1007\/3-540-09724-4"},{"key":"9360_CR10","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 9236, pp. 203\u2013220. Springer International Publishing (2015). doi: 10.1007\/978-3-319-22102-1_13","DOI":"10.1007\/978-3-319-22102-1_13"},{"issue":"1","key":"9360_CR11","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. (TOCS) 32(1), 2 (2014). doi: 10.1145\/2560537","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"9360_CR12","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207\u2013220. ACM, Big Sky, MT, USA (2009). doi: 10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"9360_CR13","doi-asserted-by":"crossref","unstructured":"Matichuk, D., Wenzel, M., Murray, T.: An Isabelle proof method language. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving\u2014-5th International Conference, ITP 2014, Vienna, Austria. Lecture Notes in Computer Science, vol. 8558. Springer (2014). doi: 10.1007\/978-3-319-08970-6_25","DOI":"10.1007\/978-3-319-08970-6_25"},{"key":"9360_CR14","doi-asserted-by":"crossref","unstructured":"Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) The Second International Conference on Certified Programs and Proofs, pp. 126\u2013142. Springer, Kyoto (2012). doi: 10.1007\/978-3-642-35308-6_12","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"9360_CR15","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL\u2014-A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer Verlag (2002). doi: 10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9360_CR16","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science. Academic Press (1990)"},{"key":"9360_CR17","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a versatile environment for human-readable formal proof documents. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"9360_CR18","unstructured":"Wenzel, M., Chaieb, A.: SML with antiquotations embedded into Isabelle\/Isar. In: Carette, J., Wiedijk, F. (eds.) Workshop on Programming Languages for Mechanized Mathematics (PLMMS 2007). Hagenberg, Austria (2007)"},{"key":"9360_CR19","doi-asserted-by":"crossref","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World, vol. 3600 (2006). doi: 10.1007\/11542384_1","DOI":"10.1007\/11542384_1"},{"key":"9360_CR20","doi-asserted-by":"crossref","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: Morrisett, G., Uustalu, T. (eds.) ICFP. ACM (2013). doi: 10.1017\/S0956796813000051","DOI":"10.1017\/S0956796813000051"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9360-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9360-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9360-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T15:42:47Z","timestamp":1567525367000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9360-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["9360"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9360-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,18]]}}}