{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:20:18Z","timestamp":1760782818688},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297352"},{"type":"electronic","value":"9783540322474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11575467_24","type":"book-chapter","created":{"date-parts":[[2005,11,11]],"date-time":"2005-11-11T13:58:51Z","timestamp":1131717531000},"page":"364-380","source":"Crossref","is-referenced-by-count":24,"title":["A Typed, Compositional Logic for a Stack-Based Abstract Machine"],"prefix":"10.1007","author":[{"given":"Nick","family":"Benton","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Proc. 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT) (1997)","DOI":"10.1007\/BFb0030634"},{"key":"24_CR2","unstructured":"Ahmed, A.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A., Felty, A.: A semantic model of types and machine instructions for proof-carrying code. In: Proc. 27th ACM Symposium on Principles of Programming Languages (POPL) (2000)","DOI":"10.1145\/325694.325727"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Appel, A., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems\u00a023(5) (2001)","DOI":"10.1145\/504709.504712"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-30142-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2004","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 34\u201349. Springer, Heidelberg (2004)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bannwart, F., Muller, P.: A program logic for bytecode. In: Proc. 1st Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE) (April 2005)","DOI":"10.1016\/j.entcs.2005.02.026"},{"key":"24_CR7","unstructured":"Benton, N.: A typed logic for stacks and jumps. Draft Note (March 2004)"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. Technical Report MSR-TR-2005-84, Microsoft Research (June 2005)","DOI":"10.1007\/11575467_24"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/11417170_8","volume-title":"Typed Lambda Calculi and Applications","author":"N. Benton","year":"2005","unstructured":"Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 86\u2013101. Springer, Heidelberg (2005)"},{"key":"24_CR10","unstructured":"Borgstr\u00f6m, J.: Translation of smart card applications for formal verification. Masters Thesis, SICS, Sweden (2002)"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: Program fragments, linking, and modularization. In: Proc. 24th ACM Symposium on Principles of Programming Languages (POPL) (1997)","DOI":"10.1145\/263699.263735"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Freund, S.N., Mitchell, J.C.: A type system for object initialization in the Java bytecode language. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a021(6) (1999)","DOI":"10.1145\/330643.330646"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Syme, D.: Typing a multi-language intermediate code. In: Proc. 28th ACM Symposium on Principles of Programming Languages (POPL) (2001)","DOI":"10.1145\/360204.360228"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-30142-4_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N.A. Hamid","year":"2004","unstructured":"Hamid, N.A., Shao, Z.: Interfacing Hoare logic and type systems for foundational proof-carrying code. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 118\u2013135. Springer, Heidelberg (2004)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: Proc. 20th IEEE Symposium on Logic in Computer Science (LICS) (2005)","DOI":"10.1109\/LICS.2005.5"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, p. 284. Springer, Heidelberg (2000)"},{"key":"24_CR17","unstructured":"Jia, L., Spalding, F., Walker, D., Glew, N.: Certifying compilation for a language with stack allocation. In: Proc. 20th IEEE Symposium on Logic in Computer Science (LICS) (2005)"},{"key":"24_CR18","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Technical Report ECS-LFCS-98-399, LFCS, University of Edinburgh (1998)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11417170_20","volume-title":"Typed Lambda Calculi and Applications","author":"S. Lindley","year":"2005","unstructured":"Lindley, S., Stark, I.: Reducibility and \u22a4\u2009\u22a4 lifting for computation types. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 262\u2013277. Springer, Heidelberg (2005)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/11417170_22","volume-title":"Typed Lambda Calculi and Applications","author":"G. Morrisett","year":"2005","unstructured":"Morrisett, G., Amal, A., Fluet, M.: L3: A linear language with locations. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 293\u2013307. Springer, Heidelberg (2005)"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. Journal of Functional Programming\u00a012(1) (2002)","DOI":"10.1017\/S0956796801004178"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a021(3) (1999)","DOI":"10.1145\/319301.319345"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL) (1997)","DOI":"10.1145\/263699.263712"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: 2nd Symposium on Operating Systems Design and Implementation (OSDI) (1996)","DOI":"10.1145\/238721.238781"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, p. 1. Springer, Heidelberg (2001)"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-45614-7_6","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"D. Oheimb von","year":"2002","unstructured":"von Oheimb, D., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, p. 89. Springer, Heidelberg (2002)"},{"key":"24_CR27","volume-title":"Higher Order Operational Techniques in Semantics","author":"A.M. Pitts","year":"1998","unstructured":"Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Higher Order Operational Techniques in Semantics. CUP, Cambridge (1998)"},{"key":"24_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, p. 162. Springer, Heidelberg (1999)"},{"key":"24_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/10930755_3","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Quigley","year":"2003","unstructured":"Quigley, C.: A programming logic for Java bytecode programs. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 41\u201354. Springer, Heidelberg (2003)"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Quigley, C.L.: A Programming Logic for Java Bytecode Programs. PhD thesis, University of Glasgow, Department of Computing Science (2004)","DOI":"10.1007\/10930755_3"},{"key":"24_CR31","unstructured":"Reynolds, J.C.: Idealized Algol and its specification logic. In: Tools and Notions for Program Construction (1982)"},{"key":"24_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, p. 366. Springer, Heidelberg (2000)"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"Stata, R., Abadi, M.: A type system for Java bytecode subroutines. In: Proc. 25th ACM Symposium on Principles of Programming Languages (POPL) (1998)","DOI":"10.1145\/268946.268959"},{"key":"24_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-46691-6_13","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"D. Oheimb von","year":"1999","unstructured":"von Oheimb, D.: Hoare logic for mutual recursion and local variables. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, p. 168. Springer, Heidelberg (1999)"},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"Vouillon, J., Mellies, P.-A.: Semantic types: A fresh look at the ideal model for types. In: Proc. 31st ACM Symposium on Principles of Programming Languages (POPL) (2004)","DOI":"10.1145\/964001.964006"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"Yu, D., Kennedy, A., Syme, D.: Formalization of generics for the.NET common language runtime. In: Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL) (2004)","DOI":"10.1145\/964001.964005"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11575467_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:57:29Z","timestamp":1605643049000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11575467_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297352","9783540322474"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/11575467_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}