{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:12:09Z","timestamp":1763467929567},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_25","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"359-374","source":"Crossref","is-referenced-by-count":14,"title":["Verified LISP Implementations on ARM,\u00a0x86\u00a0and\u00a0PowerPC"],"prefix":"10.1007","author":[{"given":"Magnus O.","family":"Myreen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael J. C.","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"25_CR1","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"R.S. Boyer","year":"1996","unstructured":"Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM\u00a043(1), 166\u2013192 (1996)","journal-title":"J. ACM"},{"issue":"11","key":"25_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1145\/362790.362798","volume":"13","author":"C.J. Cheney","year":"1970","unstructured":"Cheney, C.J.: A non-recursive list compacting algorithm. Commun. ACM\u00a013(11), 677\u2013678 (1970)","journal-title":"Commun. ACM"},{"key":"25_CR3","first-page":"54","volume-title":"Programming Language Design and Implementation (PLDI)","author":"A.J. Chlipala","year":"2007","unstructured":"Chlipala, A.J.: A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation (PLDI), pp. 54\u201365. ACM, New York (2007)"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-75560-9_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Z. Dargaye","year":"2007","unstructured":"Dargaye, Z., Leroy, X.: Mechanized verification of CPS transformations. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol.\u00a04790, pp. 211\u2013225. Springer, Heidelberg (2007)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 25\u201340. Springer, Heidelberg (2003)"},{"key":"25_CR6","unstructured":"Gordon, M.: Defining a LISP interpreter in a logic of total functions. In: The ACL2 Theorem Prover and Its Applications, ACL2 (2007)"},{"issue":"1\/2","key":"25_CR7","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01128406","volume":"8","author":"J. Guttman","year":"1995","unstructured":"Guttman, J., Ramsdell, J., Wand, M.: VLISP: A verified implementation of scheme. Lisp and Symbolic Computation\u00a08(1\/2), 5\u201332 (1995)","journal-title":"Lisp and Symbolic Computation"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-71067-7_4","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Kaufmann","year":"2008","unstructured":"Kaufmann, M., Moore, J.S.: An ACL2 tutorial. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 17\u201321. Springer, Heidelberg (2008)"},{"key":"25_CR9","first-page":"42","volume-title":"Principles of Programming Languages (POPL)","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages (POPL), pp. 42\u201354. ACM Press, New York (2006)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/978-3-540-71316-6_15","volume-title":"European Symposium on Programming (ESOP)","author":"G. Li","year":"2007","unstructured":"Li, G., Owens, S., Slind, K.: A proof-producing software compiler for a subset of higher order logic. In: European Symposium on Programming (ESOP). LNCS, pp. 205\u2013219. Springer, Heidelberg (2007)"},{"issue":"2","key":"25_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/B:JARS.0000009505.07087.34","volume":"31","author":"P. Manolios","year":"2003","unstructured":"Manolios, P., Strother Moore, J.: Partial functions in ACL2. J. Autom. Reasoning\u00a031(2), 107\u2013127 (2003)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR12","volume-title":"LISP 1.5 Programmer\u2019s Manual","author":"J. McCarthy","year":"1966","unstructured":"McCarthy, J., Abrahams, P.W., Edwards, D.J., Hart, T.P., Levin, M.I.: LISP 1.5 Programmer\u2019s Manual. The MIT Press, Cambridge (1966)"},{"key":"25_CR13","first-page":"468","volume-title":"Proceedings of the Conference on Programming Language Design and Implementation (PLDI)","author":"A. McCreight","year":"2007","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the Conference on Programming Language Design and Implementation (PLDI), pp. 468\u2013479. ACM, New York (2007)"},{"key":"25_CR14","unstructured":"Myreen, M.O.: Formal verification of machine-code programs. PhD thesis, University of Cambridge (2009)"},{"key":"25_CR15","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"M.O. Myreen","year":"2008","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures \u2013 An application of decompilation into logic. In: Formal Methods in Computer Aided Design (FMCAD). IEEE, Los Alamitos (2008)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Compiler Construction (CC)","author":"M.O. Myreen","year":"2009","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Extensible proof-producing compilation. In: Compiler Construction (CC). LNCS. Springer, Heidelberg (2009)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Pike, L., Shields, M., Matthews, J.: A verifying core for a cryptographic language compiler. In: Manolios, P., Wilding, M. (eds.) Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications. HappyJack Books (2006)","DOI":"10.1145\/1217975.1217977"},{"key":"25_CR18","volume-title":"Principles of Programming Languages (POPL)","author":"S. Sarkar","year":"2009","unstructured":"Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Myreen, T.B.M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: Principles of Programming Languages (POPL). ACM, New York (2009)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T09:00:58Z","timestamp":1552122058000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}