{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:50:46Z","timestamp":1725742246484},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_13","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"147-162","source":"Crossref","is-referenced-by-count":15,"title":["Mechanising Turing Machines and Computability Theory in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Jian","family":"Xu","sequence":"first","affiliation":[]},{"given":"Xingyuan","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32621-9_1","volume-title":"Logic, Language, Information and Computation","author":"A. Asperti","year":"2012","unstructured":"Asperti, A., Ricciotti, W.: Formalizing Turing Machines. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol.\u00a07456, pp. 1\u201325. Springer, Heidelberg (2012)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Boolos, G., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 5th edn. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511804076"},{"issue":"3","key":"13_CR3","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/362929.362947","volume":"11","author":"E.W. Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Go to Statement Considered Harmful. Communications of the ACM\u00a011(3), 147\u2013148 (1968)","journal-title":"Communications of the ACM"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Jensen, J.B., Benton, N., Kennedy, A.: High-Level Separation Logic for Low-Level Code. In: Proc.\u00a0of the 40th Symposium on Principles of Programming Languages (POPL), pp. 301\u2013314 (2013)","DOI":"10.1145\/2480359.2429105"},{"key":"13_CR5","unstructured":"Myreen, M.O.: Formal Verification of Machine-Code Programs. PhD thesis, University of Cambridge (2009)"},{"key":"13_CR6","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. Formal Aspects of Computing\u00a010, 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-22863-6_22","volume-title":"Interactive Theorem Proving","author":"M. Norrish","year":"2011","unstructured":"Norrish, M.: Mechanised Computability Theory. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 297\u2013311. Springer, Heidelberg (2011)"},{"issue":"3","key":"13_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.2307\/2269031","volume":"1","author":"E. Post","year":"1936","unstructured":"Post, E.: Finite Combinatory Processes-Formulation 1. Journal of Symbolic Logic\u00a01(3), 103\u2013105 (1936)","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/BF01418780","volume":"12","author":"R.M. Robinson","year":"1971","unstructured":"Robinson, R.M.: Undecidability and Nonperiodicity for Tilings of the Plane. Inventiones Mathematicae\u00a012, 177\u2013209 (1971)","journal-title":"Inventiones Mathematicae"},{"key":"13_CR10","unstructured":"Zammit, V.: On the Readability of Machine Checkable Formal Proofs. PhD thesis, University of Kent (1999)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T02:39:27Z","timestamp":1557974367000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}