{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T05:23:49Z","timestamp":1749792229868},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089690"},{"type":"electronic","value":"9783319089706"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08970-6_25","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T07:13:26Z","timestamp":1403939606000},"page":"390-405","source":"Crossref","is-referenced-by-count":12,"title":["An Isabelle Proof Method Language"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Matichuk","sequence":"first","affiliation":[]},{"given":"Makarius","family":"Wenzel","sequence":"additional","affiliation":[]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-31374-5_3","volume-title":"Intelligent Computer Mathematics","author":"T. Bourke","year":"2012","unstructured":"Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol.\u00a07362, pp. 32\u201348. Springer, Heidelberg (2012)"},{"issue":"6","key":"25_CR2","doi-asserted-by":"publisher","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 Notices\u00a046(6), 234 (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"25_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reasoning 3(2) (2010)","key":"25_CR5"},{"issue":"4","key":"25_CR6","doi-asserted-by":"publisher","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.\u00a023(4), 357\u2013401 (2013)","journal-title":"J. Funct. Program."},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M.J. Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-32347-8_8","volume-title":"Interactive Theorem Proving","author":"D. Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: Automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 99\u2013115. Springer, Heidelberg (2012)"},{"unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (TOCS) (to appear)","key":"25_CR9"},{"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, Big Sky, MT, USA, pp. 207\u2013220. ACM (October 2009)","key":"25_CR10","DOI":"10.1145\/1629575.1629596"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-35308-6_12","volume-title":"Certified Programs and Proofs","author":"T. Murray","year":"2012","unstructured":"Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 126\u2013142. Springer, Heidelberg (2012)"},{"unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science. Academic Press (1990)","key":"25_CR12"},{"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 (June 2007)","key":"25_CR13"},{"unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)","key":"25_CR14"},{"key":"25_CR15","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"},{"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)","key":"25_CR16","DOI":"10.1145\/2500365.2500579"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08970-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:22:20Z","timestamp":1558920140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08970-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089690","9783319089706"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08970-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}