{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:25:11Z","timestamp":1725564311327},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540205364"},{"type":"electronic","value":"9783540400189"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-40018-9_13","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T19:03:20Z","timestamp":1283713400000},"page":"178-194","source":"Crossref","is-referenced-by-count":1,"title":["Executing Verified Compiler Specification"],"prefix":"10.1007","author":[{"given":"Koji","family":"Okuma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasuhiko","family":"Minamide","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Benton, N., Kennedy, A., Russell, G.: Compiling Standard ML to Java bytecodes. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 1998), vol.\u00a034(1), pp. 129\u2013140 (1999)","DOI":"10.1145\/291251.289435"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","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., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"13_CR3","unstructured":"Bothner, P.: Kawa\u2014compiling dynamic languages to the Java VM. In: Proceedings of the USENIX, Technical Conference, FREENIX Track, New Orleans, LA, USENIX Association (1998)"},{"key":"13_CR4","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, London (1988)"},{"key":"13_CR5","unstructured":"Curzon, P.: A verified Vista implementation final report. Technical Report 311, University of Cambridge Computer Laboratory (1993)"},{"key":"13_CR6","volume-title":"Introduction to HOL : A Theorem Proving Environment for Higher Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"13_CR7","unstructured":"Hannan, J.: A type system for closure conversion. In: Proceedings of the Workshop on Types for Program Analysis, pp. 48\u201362 (1995)"},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"1133","DOI":"10.1002\/cpe.597","volume":"13","author":"G. Klein","year":"2001","unstructured":"Klein, G., Nipkow, T.: Verified lightweight bytecode verification. Concurrency and Computation: Practice and Experience\u00a013, 1133\u20131151 (2001)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified bytecode verifiers. Theoretical Computer Science\u00a0298, 583\u2013626 (2003)","journal-title":"Theoretical Computer Science"},{"key":"13_CR10","unstructured":"Meyer, J.: Jasmin home page, \n                    \n                      http:\/\/mrl.nyu.edu\/~meyer\/jasmin\/"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Minamide, Y., Morrisett, J.G., Harper, R.: Typed closure conversion. In: Proceedings of Symposium on Principles of Programming Languages, pp. 271\u2013 283 (1996)","DOI":"10.1145\/237721.237791"},{"key":"13_CR12","unstructured":"Moore, J.S.: A mechanically verified language implementation. Technical Report 30, Computational Logic Inc. (1988)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","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":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL : A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1\/2","key":"13_CR14","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BF01128408","volume":"8","author":"D.P. Oliva","year":"1995","unstructured":"Oliva, D.P., Ramsdell, J.D., Wand, M.: The VLISP verified PreScheme compiler. Lisp and Symbolic Computation\u00a08(1\/2), 111\u2013182 (1995)","journal-title":"Lisp and Symbolic Computation"},{"key":"13_CR15","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999)"},{"key":"13_CR16","volume-title":"High Integrity Compilation : a case study","author":"S. Stepney","year":"1993","unstructured":"Stepney, S.: High Integrity Compilation: a case study. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"13_CR17","unstructured":"Stringer-Calvert, D.W.: Mechanical Verification of Compiler Correctness. PhD thesis, Department of Computer Science, University of York (March 1998)"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Proceedings of International Conference on Theorem Proving in Higher Order Logics, pp. 167\u2013184 (1999)","DOI":"10.1007\/3-540-48256-3_12"},{"key":"13_CR19","unstructured":"Young, W.D.: A verified code generator for a subset of Gypsy. Technical Report 33, Computational Logic Inc. (1988)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40018-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:40:17Z","timestamp":1558287617000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40018-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205364","9783540400189"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40018-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}