{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:39:25Z","timestamp":1725586765644},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_15","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"169-183","source":"Crossref","is-referenced-by-count":5,"title":["Validated Compilation through Logic"],"prefix":"10.1007","author":[{"given":"Guodong","family":"Li","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Benton, N., Hur, C.-K.: Biorthogonality, step-indexing and compiler correctness. In: ACM International Conference on Functional programming, ICFP (2009)","DOI":"10.1145\/1596550.1596567"},{"key":"15_CR2","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., Karakostas, G. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Program verification through characteristic formulae. In: ACM International Conference on Functional Programming, ICFP (2010)","DOI":"10.1145\/1863543.1863590"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation, PLDI (2007)","DOI":"10.1145\/1250734.1250742"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: A verified compiler for an impure functional language. In: ACM Symposium on the Principles of Programming Languages, POPL (2010)","DOI":"10.1145\/1706299.1706312"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Hannan, J., Pfenning, F.: Compiler verification in LF. In: 7th Symposium on Logic in Computer Science, LICS (1992)","DOI":"10.1109\/LICS.1992.185552"},{"issue":"2-3","key":"15_CR7","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s10990-006-8746-6","volume":"19","author":"J. Hickey","year":"2006","unstructured":"Hickey, J., Nogin, A.: Formal compiler construction in a logical framework. Journal of Higher-Order and Symbolic Computation\u00a019(2-3), 197\u2013230 (2006)","journal-title":"Journal of Higher-Order and Symbolic Computation"},{"key":"15_CR8","unstructured":"The HOL-4 Theorem Prover, http:\/\/hol.sourceforge.net\/"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler backend, or: programming a compiler with a proof assistant. In: ACM Symposium on the Principles of Programming Languages, POPL (2006)","DOI":"10.1145\/1111037.1111042"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: 16th European Symposium on Programming, ESOP (2007)","DOI":"10.1007\/978-3-540-71316-6_15"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Li, G., Slind, K.: Compilation as rewriting in higher order logic. In: 21th Conference on Automated Deduction, CADE-21 (2007)","DOI":"10.1007\/978-3-540-73595-3_3"},{"key":"15_CR12","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":"15_CR13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML, Revised Edition","author":"R. Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML, Revised Edition. MIT Press, Cambridge (1997)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: ACM Symposium on the Principles of Programming Languages, POPL (2010)","DOI":"10.1145\/1706299.1706313"},{"key":"15_CR15","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.: Hoare logic for realistically modelled machine\u00a0code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 568\u2013582. Springer, Heidelberg (2007)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Machine-code verification for multiple architectures: An application of decompilation into logic. In: Formal Methods in Computer Aided Design, FMCAD (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science, LICS (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.12.020","volume":"373","author":"A. Saabas","year":"2007","unstructured":"Saabas, A., Uustalu, T.: A compositional natural semantics and hoare logic for low-level languages. Theoretical Computer Science\u00a0373(3), 273\u2013302 (2007)","journal-title":"Theoretical Computer Science"},{"key":"15_CR20","unstructured":"Slind, K.: Reasoning about Terminating Functional Programs. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"issue":"4","key":"15_CR21","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1017\/S0956796898003086","volume":"8","author":"A. Tolmach","year":"1998","unstructured":"Tolmach, A., Oliva, D.P.: From ML to Ada: Strongly-typed language interoperability via source translation. Journal of Functional Programming\u00a08(4), 367\u2013412 (1998)","journal-title":"Journal of Functional Programming"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Tristan, J.-B., Leroy, X.: Formal verification of translation validators: A case study on instruction scheduling optimizations. In: ACM Symposium on the Principles of Programming Languages, POPL (2008)","DOI":"10.1145\/1328438.1328444"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T00:07:03Z","timestamp":1560298023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}