{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:38:49Z","timestamp":1725633529147},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642353079"},{"type":"electronic","value":"9783642353086"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_2","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"4-6","source":"Crossref","is-referenced-by-count":5,"title":["Mechanized Semantics for Compiler Verification"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall (1990)"},{"key":"2_CR2","unstructured":"Milner, R.: Communicating and Mobile Systems: the pi-Calculus. Cambridge University Press (1999)"},{"issue":"1","key":"2_CR3","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: 35th symposium Principles of Programming Languages, pp. 3\u201315. ACM Press (2008)","DOI":"10.1145\/1328438.1328443"},{"issue":"5","key":"2_CR5","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems\u00a023(5), 657\u2013683 (2001)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: Operational semantics using the partiality monad. In: International Conference on Functional Programming 2012, pp. 127\u2013138. ACM Press (2012)","DOI":"10.1145\/2398856.2364546"},{"issue":"7","key":"2_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal Verification of a C Compiler Front-End. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"issue":"4","key":"2_CR10","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X. Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation\u00a0207(2), 284\u2013304 (2009)","journal-title":"Information and Computation"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"A.W. Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation Logic for Small-Step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 5\u201321. Springer, Heidelberg (2007)"},{"key":"2_CR13","unstructured":"Felleisen, M., Friedman, D.P.: Control operators, the SECD machine and the \u03bb-calculus. In: Formal Description of Programming Concepts III, pp. 131\u2013141. North-Holland (1986)"},{"issue":"46","key":"2_CR14","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C. Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science\u00a0410(46), 4747\u20134768 (2009)","journal-title":"Theoretical Computer Science"},{"key":"2_CR15","series-title":"IFIP AICT","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-15240-5_13","volume-title":"Theoretical Computer Science","author":"P.-L. Curien","year":"2010","unstructured":"Curien, P.-L., Munch-Maccagnoni, G.: The Duality of Computation under Focus. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol.\u00a0323, pp. 165\u2013181. Springer, Heidelberg (2010)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Benton, N., Hur, C.K.: Biorthogonality, step-indexing and compiler correctness. In: International Conference on Functional Programming 2009, pp. 97\u2013108. ACM Press (2009)","DOI":"10.1145\/1631687.1596567"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:13:47Z","timestamp":1620134027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}