{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:55:00Z","timestamp":1725504900313},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540786627"},{"type":"electronic","value":"9783540786634"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78663-4_6","type":"book-chapter","created":{"date-parts":[[2008,3,8]],"date-time":"2008-03-08T01:00:01Z","timestamp":1204938001000},"page":"57-72","source":"Crossref","is-referenced-by-count":2,"title":["Extending Operational Semantics of the Java Bytecode"],"prefix":"10.1007","author":[{"given":"Patryk","family":"Czarnik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksy","family":"Schubert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: Principles of Programming Languages. Association of Computing Machinery Press (2000)","DOI":"10.1145\/325694.325727"},{"key":"6_CR2","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science, Springer, Heidelberg (2004)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/11924661_24","volume-title":"Programming Languages and Systems","author":"L. Beringer","year":"2006","unstructured":"Beringer, L., Hofmann, M.: A bytecode logic for JML and types. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 389\u2013405. Springer, Heidelberg (2006)"},{"key":"6_CR4","unstructured":"Chrz\u0105szcz, J.: Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw University and University of Paris-Sud (January 2004)"},{"key":"6_CR5","unstructured":"Mobius Consortium. Deliverable\u00a03.1: Bytecode specification language and program logic (2006), http:\/\/mobius.inria.fr"},{"key":"6_CR6","unstructured":"Coq development team. The Coq proof assistant reference manual V8.0. Technical Report 255, INRIA, France, mars (2004), http:\/\/coq.inria.fr\/doc\/main.html"},{"issue":"4","key":"6_CR7","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. ACM Transactions on Programming Languages and Systems\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-61055-3_39","volume-title":"Programming Languages and Systems - ESOP \u201996","author":"S. Liang","year":"1996","unstructured":"Liang, S., Hudak, P.: Modular Denotational Semantics for Compiler Construction. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol.\u00a01058, pp. 219\u2013234. Springer, Heidelberg (1996)"},{"key":"6_CR9","unstructured":"Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Sun Microsystems, Inc. (1999), http:\/\/java.sun.com\/docs\/books\/vmspec\/"},{"key":"6_CR10","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569869","volume-title":"Action Semantics","author":"P.D. Mosses","year":"1992","unstructured":"Mosses, P.D.: Action Semantics. Cambridge Tracts in Theoretical Computer Science, vol.\u00a026. Cambridge University Press, Cambridge (1992)"},{"key":"6_CR11","first-page":"106","volume-title":"Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106\u2013119. Association of Computing Machinery Press, New York, NY, USA (1997)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48092-7_6","volume-title":"Correct System Design","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R.: Type and effect systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol.\u00a01710, pp. 114\u2013136. Springer, Heidelberg (1999)"},{"key":"6_CR13","unstructured":"Pichardie, D.: Bicolano \u2013 Byte Code Language in Coq (2006), http:\/\/mobius.inia.fr\/bicolano"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-540-30477-7_8","volume-title":"Programming Languages and Systems","author":"C. Skalka","year":"2004","unstructured":"Skalka, C., Smith, S.F.: History effects and verification. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol.\u00a03302, pp. 107\u2013128. Springer, Heidelberg (2004)"},{"key":"6_CR15","unstructured":"Sun Microsystems Inc., 4150 Network Circle, Santa Clara, California 95054. Connected Limited Device Configuration. Specification Version 1.1. JavaTM 2 Platform, Micro Edition (J2METM) (March 2003), http:\/\/jcp.org\/aboutJava\/communityprocess\/final\/jsr139\/index.html"},{"issue":"1","key":"6_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M. Tofte","year":"1990","unstructured":"Tofte, M.: Type Inference for Polymorphic References. Information and Computation\u00a089(1), 1\u201334 (1990)","journal-title":"Information and Computation"},{"issue":"2","key":"6_CR17","first-page":"109","volume":"132","author":"M. Tofte","year":"1997","unstructured":"Tofte, M., Talpin, J.-P.: Region-Based Memory Management. IC\u00a0132(2), 109\u2013176 (1997)","journal-title":"IC"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78663-4_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:17:53Z","timestamp":1619507873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78663-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540786627","9783540786634"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78663-4_6","relation":{},"subject":[]}}