{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:00:58Z","timestamp":1725490858623},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_3","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"19-34","source":"Crossref","is-referenced-by-count":8,"title":["Compilation as Rewriting in Higher Order Logic"],"prefix":"10.1007","author":[{"given":"Guodong","family":"Li","sequence":"first","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Tofte, M., Vejlstrup, M.: From region inference to von neumann machines via region representation inference. In: 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201996) (1996)","DOI":"10.1145\/237721.237771"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"issue":"6","key":"3_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. ACM SIGSOFT Software Engineering Notes\u00a028(6), 2\u20132 (2003)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: ACM SIGPLAN-SIGACT 93 Conference on Programming Language Design and Implementation (PLDI 1993) (1993)","DOI":"10.1145\/155090.155113"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Gordon, M., Iyoda, J., Owens, S., Slind, K.: Automatic formal synthesis of hardware from higher order logic. In: Proceedings of Fifth International Workshop on Automated Verification of Critical Systems (AVoCS 2005), ENTCS, vol. 145 (2005)","DOI":"10.1016\/j.entcs.2005.10.003"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Hannan, J., Pfenning, F.: Compiler verification in LF. In: Proceedings of the 7th Symposium on Logic in Computer Science (LICS 1992) (1992)","DOI":"10.1109\/LICS.1992.185552"},{"issue":"2-3","key":"3_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":"3_CR8","unstructured":"Resler, R., Boyle, J., Winter, K.: Do you trust your compiler? applying formal methods to constructing high-assurance compilers, High-Assurance Systems Engineering Workshop (1997)"},{"issue":"4","key":"3_CR9","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. TOPLAS\u00a028(4), 619\u2013695 (2006)","journal-title":"TOPLAS"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: Code generation and implementation correctnes. In: 4th IEEE International Conference on Software Engineering and Formal Methods (2005)","DOI":"10.1109\/SEFM.2005.51"},{"key":"3_CR11","volume-title":"Symposium on the Principles of Programming Languages (POPL 2006)","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler backend, or: programming a compiler with a proof assistant. In: Symposium on the Principles of Programming Languages (POPL 2006), ACM Press, New York (2006)"},{"key":"3_CR12","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) (2007)","DOI":"10.1007\/978-3-540-71316-6_15"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Liang, C.C.: Compiler construction in higher order logic programming, Practical Aspects of Declarative Languages (2002)","DOI":"10.1007\/3-540-45587-6_5"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"key":"3_CR15","series-title":"Automated Reasoning Series","volume-title":"Piton: A mechanically verified assembly-level language","author":"J.S. Moore","year":"1996","unstructured":"Moore, J.S.: Piton: A mechanically verified assembly-level language. Automated Reasoning Series. Kluwer Academic Publishers, Dordrecht (1996)"},{"issue":"3","key":"3_CR16","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. TOPLAS\u00a021(3), 527\u2013568 (1999)","journal-title":"TOPLAS"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1093\/comjnl\/45.1.37","volume":"45","author":"M. Norrish","year":"2002","unstructured":"Norrish, M., Slind, K.: A thread of HOL development. The Computer Journal\u00a045(1), 37\u201345 (2002)","journal-title":"The Computer Journal"},{"key":"3_CR19","unstructured":"Norrish, M., Slind, K.: HOL-4 manuals (1998-2006) , Available at http:\/\/hol.sourceforge.net\/"},{"key":"3_CR20","unstructured":"Saabas, A., Uustalu, T.: A compositional natural semantics and hoare logic for low- level languages, SOS 2005 (2005)"},{"key":"3_CR21","series-title":"amast series in computing","doi-asserted-by":"crossref","DOI":"10.1142\/2870","volume-title":"An algebraic approach to compiler design.","author":"A. Sampaio","year":"1997","unstructured":"Sampaio, A.: An algebraic approach to compiler design. amast series in computing, vol.\u00a04. World Scientific, Singapore (1997)"},{"key":"3_CR22","unstructured":"Slind, K.: Reasoning about terminating functional programs, Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Tan","year":"2005","unstructured":"Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, Springer, Heidelberg (2005)"},{"issue":"4","key":"3_CR24","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/567097.567099","volume":"24","author":"M.v.d. Brand","year":"2003","unstructured":"Brand, M.v.d., Heering, J., Klint, P., Olivier, P.A.: Compiling language definitions: The ASF+SDF compiler. ACM Transactions of Programming Language Systems\u00a024(4), 334\u2013368 (2003)","journal-title":"ACM Transactions of Programming Language Systems"},{"key":"3_CR25","unstructured":"Winter, V.L.: Program transformation in hats. In: Proceedings of the Software Transformation Systems Workshop (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:08Z","timestamp":1619517188000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}