{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:32:44Z","timestamp":1743078764345,"version":"3.40.3"},"publisher-location":"Cham","reference-count":8,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319218182"},{"type":"electronic","value":"9783319218199"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21819-9_22","type":"book-chapter","created":{"date-parts":[[2015,8,3]],"date-time":"2015-08-03T11:16:31Z","timestamp":1438600591000},"page":"290-300","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalisation vs. Understanding"],"prefix":"10.1007","author":[{"given":"Declan","family":"Thompson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,4]]},"reference":[{"key":"22_CR1","unstructured":"Isabelle hompage. http:\/\/isabelle.in.tum.de\/"},{"key":"22_CR2","unstructured":"Ballarin, C., Belgrade 2008 - Tutorial: Introduction to the proof assistant. http:\/\/www21.in.tum.de\/ ballarin\/belgrade08-tut\/"},{"key":"22_CR3","first-page":"1001","volume":"21","author":"CS Calude","year":"2014","unstructured":"Calude, C.S., Desfontaines, D.: Universality and almost decidability. Fundamenta Informaticae 21, 1001\u20131006 (2014)","journal-title":"Fundamenta Informaticae"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-02614-0_20","volume-title":"Intelligent Computer Mathematics","author":"CS Calude","year":"2009","unstructured":"Calude, C.S., M\u00fcller, C.: Formal proof: reconciling correctness and understanding. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 217\u2013232. Springer, Heidelberg (2009)"},{"key":"22_CR5","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proof, Language, and Interaction","author":"M Gordon","year":"2000","unstructured":"Gordon, M.: From LCF to HOL: a short history. In: Plotkin, G., Stirling, C.P., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 169\u2013186. MIT Press, Cambridge (2000)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Programming and proving in Isabelle\/HOL (2013)","DOI":"10.1007\/978-3-319-10542-0_6"},{"key":"22_CR7","unstructured":"OED Online. proof, n. http:\/\/www.oed.com\/view\/Entry\/152578?rskey=bJkM38, October 2014"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-39634-2_13","volume-title":"Interactive Theorem Proving","author":"J Xu","year":"2013","unstructured":"Xu, J., Zhang, X., Urban, C.: Mechanising turing machines and computability theory in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147\u2013162. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Unconventional Computation and Natural Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21819-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T09:52:17Z","timestamp":1718013137000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21819-9_22"}},"subtitle":["A Case Study in Isabelle"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319218182","9783319218199"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21819-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"4 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}