{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T09:38:07Z","timestamp":1787564287151,"version":"build-2736575974"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540418627","type":"print"},{"value":"9783540453093","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45309-1_23","type":"book-chapter","created":{"date-parts":[[2008,11,27]],"date-time":"2008-11-27T19:39:26Z","timestamp":1227814766000},"page":"352-366","source":"Crossref","is-referenced-by-count":7,"title":["Proof-Directed De-compilation of Low-Level Code"],"prefix":"10.1007","author":[{"given":"Shin-ya","family":"Katsumata","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Atsushi","family":"Ohori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"S. Freund and J. Mitchell. A type system for object initialization in the Java byte code language. In Proc. OOPSLA\u201998, pages 310\u2013328, 1998.","DOI":"10.1145\/286936.286972"},{"key":"23_CR2","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(93)90011-H","volume":"110","author":"J. Gallier","year":"1993","unstructured":"J. Gallier. Constructive logics part I: A tutorial on proof systems and typed \u03bb-calculi. Theoretical Computer Science 110, pages 249\u2013339, 1993.","journal-title":"Theoretical Computer Science"},{"key":"23_CR3","unstructured":"J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996."},{"key":"23_CR4","unstructured":"T. Lindholm and F. Yellin. The Java virtual machine specification. AddisonWesley, 2nd edition, 1999."},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"J. Meyer and T. Downing. Java Virtual Machine. O\u2019Reilly, 1997.","DOI":"10.1016\/S1353-4858(97)83033-4"},{"key":"23_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Proc. Types in Compilation","author":"G. Morrisett","year":"1998","unstructured":"G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In Proc. Types in Compilation, LNCS 1473, pages 28\u201352, 1998."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. In Proc. POPL\u201998, pages 85\u201397, 1998.","DOI":"10.1145\/268946.268954"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"G. Necula. Proof-carrying code. In Proc. POPL\u201998, pages 106\u2013119, 1998.","DOI":"10.1145\/263699.263712"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"R. O\u2019Callahan. A simple, comprehensive type system for Java bytecode subroutines. In Proc. POPL\u201999, pages 70\u201378, 1999.","DOI":"10.1145\/292540.292549"},{"key":"23_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-48959-2_20","volume-title":"Proc. TLCA\u201999","author":"A. Ohori","year":"1999","unstructured":"A. Ohori. A Curry-Howard isomorphism for compilation and program execution. In Proc. TLCA\u201999, LNCS 1581, pages 280\u2013294, 1999."},{"key":"23_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/10705424_20","volume-title":"Proc. FLOPS\u201999","author":"A. Ohori","year":"1999","unstructured":"A. Ohori. The logical abstract machine: a Curry-Howard isomorphism for machine code. In Proc. FLOPS\u201999, LNCS 1722, pages 300\u2013318,1999."},{"key":"23_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-58085-9_83","volume-title":"Proc. Types for Proofs and Program","author":"C. Raffalli","year":"1994","unstructured":"C. Raffalli. Machine deduction. In Proc. Types for Proofs and Program, LNCS 806, pages 333\u2013351, 1994."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proc. POPL\u201998, pages 149\u2013160, 1998.","DOI":"10.1145\/268946.268959"},{"key":"23_CR14","unstructured":"Proceedings of Working Conference on Reverse Engineering. IEEE Computer Society Press, 1993-."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45309-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,4]],"date-time":"2025-02-04T16:04:29Z","timestamp":1738685069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45309-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418627","9783540453093"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45309-1_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}