{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:53:47Z","timestamp":1725573227097},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540254355"},{"type":"electronic","value":"9783540319870"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31987-0_19","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T18:42:00Z","timestamp":1292870520000},"page":"263-278","source":"Crossref","is-referenced-by-count":3,"title":["Denotational Semantics for Abadi and Leino\u2019s Logic of Objects"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Reus","sequence":"first","affiliation":[]},{"given":"Jan","family":"Schwinghammer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer, New York (1996)"},{"key":"19_CR2","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-540-39910-0_2","volume-title":"Verification: Theory and Practice","author":"M. Abadi","year":"2004","unstructured":"Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Dershowitz, N. (ed.) Verification: Theory and Practice, pp. 11\u201341. Springer, Heidelberg (2004)"},{"issue":"4","key":"19_CR3","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"R.M. Amadio","year":"1993","unstructured":"Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems\u00a015(4), 575\u2013631 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"19_CR4","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K.R. Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: A survey \u2014 part I. ACM Transactions on Programming Languages and Systems\u00a03(4), 431\u2013483 (1981)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-49019-1_10","volume-title":"Foundations of Software Science and Computation Structures","author":"F.S. Boer de","year":"1999","unstructured":"de Boer, F.S.: A WP-calculus for OO. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 135\u2013149. Springer, Heidelberg (1999)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BFb0053566","volume-title":"Programming Languages and Systems","author":"U. Hensel","year":"1998","unstructured":"Hensel, U., Huisman, M., Jacobs, B., Tews, H.: Reasoning about classes in object-oriented languages: Logical models and tools. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol.\u00a01381, pp. 105\u2013121. Springer, Heidelberg (1998)"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis of Computer Programming. Communications of the ACM\u00a012, 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"19_CR8","unstructured":"Hofmann, M., Tang, F.: Generation of verification conditions for Abadi and Leino\u2019s logic of objects. In: Presented at 9th International Workshop on Foundations of Object-Oriented Languages (2002)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/BFb0053570","volume-title":"Programming Languages and Systems","author":"K. Rustan","year":"1998","unstructured":"Rustan, K., Leino, M.: Recursive object types in a logic of object-oriented programs. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol.\u00a01381, pp. 170\u2013184. Springer, Heidelberg (1998)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-45793-3_16","volume-title":"Computer Science Logic","author":"P.B. Levy","year":"2002","unstructured":"Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, p. 232. Springer, Heidelberg (2002)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Logic and Computation: Interactive proof with Cambridge LCF. In: Cambridge Tracts in Theoretical Computer Science, vol.\u00a02 (1987)","DOI":"10.1017\/CBO9780511526602"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A.M. Pitts","year":"1996","unstructured":"Pitts, A.M.: Relational properties of domains. Information and Computation\u00a0127, 66\u201390 (1996)","journal-title":"Information and Computation"},{"key":"19_CR13","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, pp. 162\u2013176. Springer, Heidelberg (1999)"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1006\/inco.2001.2927","volume":"172","author":"U.S. Reddy","year":"2002","unstructured":"Reddy, U.S.: Objects and classes in algol-like languages. Information and Computation\u00a0172(1), 63\u201397 (2002)","journal-title":"Information and Computation"},{"issue":"1\u20133","key":"19_CR15","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.scico.2004.01.007","volume":"50","author":"U.S. Reddy","year":"2004","unstructured":"Reddy, U.S., Yang, H.: Correctness of data representations involving heap data structures. Science of Computer Programming\u00a050(1\u20133), 129\u2013160 (2004)","journal-title":"Science of Computer Programming"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/3-540-45719-4_32","volume-title":"Algebraic Methodology and Software Technology","author":"B. Reus","year":"2002","unstructured":"Reus, B.: Class-based versus object-based: A denotational comparison. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 473\u2013488. Springer, Heidelberg (2002)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-540-45220-1_37","volume-title":"Computer Science Logic","author":"B. Reus","year":"2003","unstructured":"Reus, B.: Modular semantics and logics of classes. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol.\u00a02803, pp. 456\u2013469. Springer, Heidelberg (2003)"},{"key":"19_CR18","unstructured":"Reus, B., Schwinghammer, J.: Denotational semantics for Abadi and Leino\u2019s logic of objects. Technical Report 2004:03, Informatics, University of Sussex (2004)"},{"key":"19_CR19","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.tcs.2004.01.030","volume":"316","author":"B. Reus","year":"2004","unstructured":"Reus, B., Streicher, T.: Semantics and logic of object calculi. Theoretical Computer Science\u00a0316, 191\u2013213 (2004)","journal-title":"Theoretical Computer Science"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/3-540-45314-8_22","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Reus","year":"2001","unstructured":"Reus, B., Wirsing, M., Hennicker, R.: A Hoare-Calculus for Verifying Java Realizations of OCL-Constrained Design Models. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 300\u2013317. Springer, Heidelberg (2001)"},{"issue":"13","key":"19_CR21","doi-asserted-by":"publisher","first-page":"1173","DOI":"10.1002\/cpe.598","volume":"13","author":"D. Oheimb von","year":"2001","unstructured":"von Oheimb, D.: Hoare logic for Java in Isabelle\/HOL. Concurrency and Computation: Practice and Experience\u00a013(13), 1173\u20131214 (2001)","journal-title":"Concurrency and Computation: Practice and Experience"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31987-0_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:33:19Z","timestamp":1605760399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31987-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540254355","9783540319870"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31987-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}