{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:43Z","timestamp":1725516523154},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642326202"},{"type":"electronic","value":"9783642326219"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32621-9_1","type":"book-chapter","created":{"date-parts":[[2012,8,18]],"date-time":"2012-08-18T10:40:40Z","timestamp":1345286440000},"page":"1-25","source":"Crossref","is-referenced-by-count":7,"title":["Formalizing Turing Machines"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/j.procs.2011.09.054","volume":"7","author":"R. Amadio","year":"2011","unstructured":"Amadio, R., Asperti, A., Ayache, N., Campbell, B., Mulligan, D., Pollack, R., R\u00e9gis-Gianas, Y., Coen, C.S., Stark, I.: Certified complexity. Procedia CS\u00a07, 175\u2013177 (2011)","journal-title":"Procedia CS"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Arora, S., Barak, B.: Computational Complexity: A Modern Approach. Cambridge Univ. Press (2009)","DOI":"10.1017\/CBO9780511804090"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Asperti, A.: The intensional content of rice\u2019s theorem. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Francisco, California, USA, January 7-12, pp. 113\u2013119. ACM (2008)","DOI":"10.1145\/1328438.1328455"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-14128-7_13","volume-title":"Intelligent Computer Mathematics","author":"A. Asperti","year":"2010","unstructured":"Asperti, A., Sacerdoti Coen, C.: Some Considerations on the Usability of Interactive Provers. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 147\u2013156. Springer, Heidelberg (2010)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Asperti, A., Avigad, J. (eds.): Special issue on interactive theorem proving and the formalisation of mathematics. Mathematical Structures in Computer Science, vol.\u00a021(4) (2011)","DOI":"10.1017\/S0960129511000065"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/978-3-642-31374-5_28","volume-title":"CICM 2012","author":"A. Asperti","year":"2012","unstructured":"Asperti, A., Ricciotti, W.: A Web Interface for Matita. In: Jeuring, J. (ed.) CICM 2012. LNCS, vol.\u00a07362, pp. 417\u2013421. Springer, Heidelberg (2012)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in Unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 84\u201398. Springer, Heidelberg (2009)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-22438-6_7","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Asperti","year":"2011","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita Interactive Theorem Prover. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 64\u201369. Springer, Heidelberg (2011)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Log.\u00a09(1) (2007)","DOI":"10.1145\/1297658.1297660"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, pp. 3\u201315. ACM (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"1_CR11","unstructured":"Davis, M.: Computability and Unsolvability. Dover Publications (1985)"},{"issue":"4","key":"1_CR12","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/321356.321362","volume":"13","author":"R.E. Stearns","year":"1966","unstructured":"Stearns, R.E., Hennie, F.C.: Two-tape simulation of multi tape turing machines. Journal of ACM\u00a013(4), 533\u2013546 (1966)","journal-title":"Journal of ACM"},{"issue":"4","key":"1_CR13","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321296.321308","volume":"12","author":"P.C. Fischer","year":"1965","unstructured":"Fischer, P.C.: On formalisms for turing machines. J. ACM\u00a012(4), 570\u2013580 (1965)","journal-title":"J. ACM"},{"key":"1_CR14","unstructured":"Hales, T., Gonthier, G., Harrison, J., Wiedijk, F.: A Special Issue on Formal Proof. Notices of the American Mathematical Society\u00a055 (2008)"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1090\/S0002-9947-1965-0170805-7","volume":"117","author":"J. Hartmanis","year":"1965","unstructured":"Hartmanis, J., Stearns, R.E.: On the computational complexity of algorithms. Transaction of the American Mathematical Society\u00a0117, 285\u2013306 (1965)","journal-title":"Transaction of the American Mathematical Society"},{"issue":"6","key":"1_CR16","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1016\/S0019-9958(65)90399-2","volume":"8","author":"F.C. Hennie","year":"1965","unstructured":"Hennie, F.C.: One-tape, off-line turing machine computations. Information and Control\u00a08(6), 553\u2013578 (1965)","journal-title":"Information and Control"},{"key":"1_CR17","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley (1979)"},{"issue":"1","key":"1_CR18","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G. Klein","year":"2009","unstructured":"Klein, G.: Operating system verification \u2013 an overview. Sadhana\u00a034(1), 27\u201369 (2009)","journal-title":"Sadhana"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proc. of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, pp. 42\u201354 (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"1_CR20","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)"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Sipser, M.: Introduction to the Theory of Computation. PWS (1996)","DOI":"10.1145\/230514.571645"},{"issue":"42","key":"1_CR22","first-page":"230","volume":"2","author":"A.M. Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the entscheidungsproblem. Proc. of the London Math. Society\u00a02(42), 230\u2013265 (1936)","journal-title":"Proc. of the London Math. Society"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"van Emde Boas, P.: Machine models and simulation. In: Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity (A), pp. 1\u201366 (1990)","DOI":"10.1016\/B978-0-444-88071-0.50006-0"},{"key":"1_CR24","unstructured":"Weirich, S., Pierce, B. (eds.): Special issue on the poplmark challenge. Journal of Automated Reasoning (2011) (published online)"},{"issue":"12","key":"1_CR25","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/2043174.2043197","volume":"54","author":"J. Yang","year":"2011","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. Commun. ACM\u00a054(12), 123\u2013131 (2011)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32621-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T03:17:41Z","timestamp":1557199061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32621-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642326202","9783642326219"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32621-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}