{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:52Z","timestamp":1749124072470},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_27","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T22:48:36Z","timestamp":1180651716000},"page":"403-417","source":"Crossref","is-referenced-by-count":2,"title":["Investigating Type-Certifying Compilation with Isabelle"],"prefix":"10.1007","author":[{"given":"Martin","family":"Strecker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"27_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TYPES Working Group Annual Meeting 2000","author":"S. Berghofer","year":"2000","unstructured":"Stefan Berghofer and Tobias Nipkow. Executing higher order logic. In Proc. TYPES Working Group Annual Meeting 2000, LNCS, 2000. Available from http:\/\/www4.in.tum.de\/~berghofe\/papers\/TYPES2000.pdf ."},{"issue":"13","key":"27_CR2","doi-asserted-by":"publisher","first-page":"1133","DOI":"10.1002\/cpe.597","volume":"13","author":"G. Klein","year":"2001","unstructured":"Gerwin Klein and Tobias Nipkow. Verified lightweight bytecode verification. Concurrency and Computation: Practice and Experience, 13(13):1133\u20131151, 2001. Invited contribution to special issue on Formal Techniques for Java.","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Gerwin Klein and Tobias Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 2002. to appear.","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"27_CR4","unstructured":"Greg Morrisett. Compiling with Types. PhD thesis, CMU, December 1995."},{"key":"27_CR5","unstructured":"Tobias Nipkow, David von Oheimb, and Cornelia Pusch. \u03bcJava: Embedding a programming language in a theorem prover. In F.L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999, pages 117\u2013144. IOS Press, 2000."},{"key":"27_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL. A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle\/HOL. A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, 2002."},{"key":"27_CR7","unstructured":"David von Oheimb. Analyzing Java in Isabelle\/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, 2001. http:\/\/www4.in.tum.de\/~oheimb\/diss\/ ."},{"key":"27_CR8","unstructured":"E. Rose and K. H. Rose. Lightweight bytecode verification. In Workshop \u201cFormal Underpinnings of the Java Paradigm\u201d, OOPSLA\u201998, 1998."},{"key":"27_CR9","volume-title":"Technical report","author":"R. F. St\u00e4rk","year":"2001","unstructured":"R. F. St\u00e4rk and J. Schmid. The problem of bytecode verification in current implementations of the JVM. Technical report, Department of Computer Science, ETH Z\u00fcrich, Switzerland, 2001."},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"R. St\u00e4rk, J. Schmid, and E. B\u00f6rger. Java and the Java Virtual Machine-Definition, Verification, Validation. Springer Verlag, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"key":"27_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Proc. CADE","author":"M. Strecker","year":"2002","unstructured":"Martin Strecker. Formal verification of a Java compiler in Isabelle. In Proc. CADE, volume 2392 of LNCS, pages 63\u201377. Springer Verlag, 2002."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:17:58Z","timestamp":1556450278000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}