{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:26:48Z","timestamp":1750670808117,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642007217"},{"type":"electronic","value":"9783642007224"}],"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-00722-4_2","type":"book-chapter","created":{"date-parts":[[2009,3,26]],"date-time":"2009-03-26T21:00:16Z","timestamp":1238101216000},"page":"2-16","source":"Crossref","is-referenced-by-count":12,"title":["Extensible Proof-Producing Compilation"],"prefix":"10.1007","author":[{"given":"Magnus O.","family":"Myreen","sequence":"first","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]},{"given":"Michael J. C.","family":"Gordon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"The Netwide Assembler, http:\/\/www.nasm.us\/"},{"key":"2_CR2","unstructured":"The GNU Project. GCC, the GNU Compiler Collection, http:\/\/gcc.gnu.org\/"},{"key":"2_CR3","first-page":"1","volume-title":"Principles and Practice of Declarative Programming (PPDP)","author":"N. Benton","year":"2007","unstructured":"Benton, N., Zarfaty, U.: Formalizing and verifying semantic type soundness of a simple compiler. In: Leuschel, M., Podelski, A. (eds.) Principles and Practice of Declarative Programming (PPDP), pp. 1\u201312. ACM, New York (2007)"},{"issue":"11","key":"2_CR4","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":"2_CR5","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":"2_CR6","doi-asserted-by":"crossref","unstructured":"Crary, K., Sarkar, S.: Foundational certified code in a metalogical framework. Technical Report CMU-CS-03-108, Carnegie Mellon University (2003)","DOI":"10.1007\/978-3-540-45085-6_9"},{"key":"2_CR7","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":"2_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.entcs.2005.10.003","volume":"145","author":"M. Gordon","year":"2006","unstructured":"Gordon, M., Iyoda, J., Owens, S., Slind, K.: Automatic formal synthesis of hardware from higher order logic. Electr. Notes Theor. Comput. Sci.\u00a0145, 27\u201343 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1\/2","key":"2_CR9","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"},{"issue":"4","key":"2_CR10","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst.\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR11","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":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-71316-6_15","volume-title":"Programming Languages and Systems","author":"G.-D. Li","year":"2007","unstructured":"Li, G.-D., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 205\u2013219. Springer, Heidelberg (2007)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-73595-3_3","volume-title":"Automated Deduction \u2013 CADE-21","author":"G.-D. Li","year":"2007","unstructured":"Li, G.-D., Slind, K.: Compilation as rewriting in higher order logic. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 19\u201334. Springer, Heidelberg (2007)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/978-3-540-78800-3_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Li","year":"2008","unstructured":"Li, G., Slind, K.: Trusted source translation of a total function language. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 471\u2013485. Springer, Heidelberg (2008)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/11617990_13","volume-title":"Types for Proofs and Programs","author":"T. Meyer","year":"2006","unstructured":"Meyer, T., Wolff, B.: Tactic-based optimized compilation of functional programs. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 201\u2013214. Springer, Heidelberg (2006)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-75698-9_18","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"M.O. Myreen","year":"2007","unstructured":"Myreen, M.O., Fox, A.C.J., Gordon, M.J.C.: A Hoare logic for ARM machine code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol.\u00a04767, pp. 272\u2013286. Springer, Heidelberg (2007)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-540-71209-1_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.O. Myreen","year":"2007","unstructured":"Myreen, M.O., Gordon, M.J.C.: A Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 568\u2013582. Springer, Heidelberg (2007)"},{"key":"2_CR18","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":"2_CR19","first-page":"83","volume-title":"Programming Language Design and Implementation (PLDI)","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation (PLDI), pp. 83\u201394. ACM, New York (2000)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Compiler Construction","author":"M.C. Rinard","year":"1999","unstructured":"Rinard, M.C.: Credible compilation. In: J\u00e4hnichen, S. (ed.) CC 1999. LNCS, vol.\u00a01575. Springer, Heidelberg (1999)"},{"key":"2_CR22","first-page":"17","volume-title":"Principles of Programming Languages (POPL)","author":"J.-B. Tristan","year":"2008","unstructured":"Tristan, J.-B., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. In: Principles of Programming Languages (POPL), pp. 17\u201327. ACM, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Compiler Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00722-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T23:51:01Z","timestamp":1558223461000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00722-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642007217","9783642007224"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00722-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}