{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:20Z","timestamp":1725511880237},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540713142"},{"type":"electronic","value":"9783540713166"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-71316-6_15","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:58:28Z","timestamp":1184590708000},"page":"205-219","source":"Crossref","is-referenced-by-count":12,"title":["Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic"],"prefix":"10.1007","author":[{"given":"Guodong","family":"Li","sequence":"first","affiliation":[]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., et al. (eds.) TYPES 2000. LNCS, vol.\u00a02277, Springer, Heidelberg (2002)"},{"key":"15_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)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_20","volume-title":"Formal Methods and Software Engineering","author":"S. Blazy","year":"2005","unstructured":"Blazy, S., Leroy, X.: Formal verification of a memory model for C-like imperative languages. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, Springer, Heidelberg (2005)"},{"issue":"6","key":"15_CR4","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 (2003)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1145\/1133981.1134028","volume-title":"ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI\u201906)","author":"X. Feng","year":"2006","unstructured":"Feng, X., et al.: Modular verification of assembly code with stack-based control abstractions. In: ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI\u201906), pp. 401\u2013414. ACM Press, New York (2006)"},{"key":"15_CR6","unstructured":"Fox, A.: Formal verification of the ARM6 micro-architecture. Tech. Report 548, University of Cambridge Computer Laboratory (November 2002)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Gordon, M., et al.: 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.\u00a0145 (2005)","DOI":"10.1016\/j.entcs.2005.10.003"},{"issue":"2-3","key":"15_CR8","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"},{"issue":"4","key":"15_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":"15_CR10","volume-title":"4th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006)","author":"D. Leinenbach","year":"2005","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 (SEFM 2006), IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"15_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":"15_CR12","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5625.001.0001","volume-title":"Programming with constraints, an introduction","author":"K. Marriott","year":"1998","unstructured":"Marriott, K., Stuckey, P.J.: Programming with constraints, an introduction. MIT Press, Cambridge (1998)"},{"key":"15_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/11916277_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Matthews","year":"2006","unstructured":"Matthews, J., et al.: Verification Condition Generation Via Theorem Proving. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 362\u2013376. Springer, Heidelberg (2006)"},{"key":"15_CR14","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":"15_CR15","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., et al.: From System F to typed assembly language. ACM Transactions on Programming Languages and Systems\u00a021(3), 527\u2013568 (1999), citeseer.ist.psu.edu\/morrisett98from.html","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR16","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.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"15_CR17","unstructured":"Norrish, M., Slind, K.: HOL-4 manuals (1998-2006), Available at http:\/\/hol.sourceforge.net\/"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.D., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, Springer, Heidelberg (1998)"},{"key":"15_CR19","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"IEEE Symposium on Logic in Computer Science (LICS\u201902)","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science (LICS\u201902), pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"15_CR20","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":"15_CR21","unstructured":"Slind, K.: Reasoning about terminating functional programs. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods and Software Engineering","author":"G. Watson","year":"2003","unstructured":"Watson, G.: Compilation by refinement for a practical assembly language. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, Springer, Heidelberg (2003)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Fast Software Encryption","author":"D. Wheeler","year":"1995","unstructured":"Wheeler, D., Needham, R.: TEA, a tiny encryption algorithm. In: Preneel, B. (ed.) FSE 1994. LNCS, vol.\u00a01008, Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71316-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:49:43Z","timestamp":1556668183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71316-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540713142","9783540713166"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71316-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}