{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:04:55Z","timestamp":1725541495206},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642106712"},{"type":"electronic","value":"9783642106729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10672-9_14","type":"book-chapter","created":{"date-parts":[[2009,12,2]],"date-time":"2009-12-02T09:08:11Z","timestamp":1259744891000},"page":"178-193","source":"Crossref","is-referenced-by-count":3,"title":["Weak updates and separation logic"],"prefix":"10.1007","author":[{"given":"Gang","family":"Tan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongxu","family":"Cai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Ahmed, A.J.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)"},{"issue":"5","key":"14_CR2","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. on Prog. Lang. and Sys.\u00a023(5), 657\u2013683 (2001)","journal-title":"ACM Trans. on Prog. Lang. and Sys."},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/1190216.1190235","volume-title":"POPL 2007","author":"A.W. Appel","year":"2007","unstructured":"Appel, A.W., Mellies, P.-A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL 2007, pp. 109\u2013122. ACM Press, New York (2007)"},{"issue":"4","key":"14_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1377492.1377493","volume":"30","author":"M. Furr","year":"2008","unstructured":"Furr, M., Foster, J.S.: Checking type safety of foreign function calls. ACM Trans. Program. Lang. Syst.\u00a030(4), 1\u201363 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"14_CR5","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/0020-0190(95)00178-6","volume":"57","author":"R. Harper","year":"1996","unstructured":"Harper, R.: A simplified account of polymorphic references. Information Processing Letters\u00a057(1), 15\u201316 (1996)","journal-title":"Information Processing Letters"},{"issue":"10","key":"14_CR6","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 578\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order frame rules. In: LICS 2005, June 2005, pp. 270\u2013279 (2005)","DOI":"10.1109\/LICS.2005.5"},{"key":"14_CR8","unstructured":"Krishnaswami, N., Birkedal, L., Aldrich, J., Reynolds, J.: Idealized ML and its separation logic (July 2007)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. In: Proc. 34th ACM Symp. on Principles of Prog. Lang., pp. 3\u201310 (2007)","DOI":"10.1145\/1190216.1190220"},{"key":"14_CR10","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. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"14_CR11","unstructured":"Parkinson, M.: Local reasoning for Java. PhD thesis, University of Cambridge Computer Laboratory, Oxford. Tech Report UCAM-CL-TR-654 (November 2005)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/11874683_38","volume-title":"Computer Science Logic","author":"B. Reus","year":"2006","unstructured":"Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 575\u2013590. Springer, Heidelberg (2006)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS 2002, July 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"14_CR14","unstructured":"Tan, G., Croft, J.: An empirical security study of the native code in the JDK. In: 17th Usenix Security Symposium, pp. 365\u2013377 (2008)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Tan, G., Shao, Z., Feng, X., Cai, H.: Weak updates and separation logic (June 2009), http:\/\/www.cse.lehigh.edu\/~gtan\/paper\/WUSL-tr.pdf","DOI":"10.1007\/978-3-642-10672-9_14"},{"issue":"1","key":"14_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. Inf. and Comp.\u00a089(1), 1\u201334 (1990)","journal-title":"Inf. and Comp."},{"issue":"2","key":"14_CR17","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M. Tofte","year":"1997","unstructured":"Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation\u00a0132(2), 109\u2013176 (1997)","journal-title":"Information and Computation"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/3-540-49099-X_9","volume-title":"Programming Languages and Systems","author":"V. Trifonov","year":"1999","unstructured":"Trifonov, V., Shao, Z.: Safe and principled language interoperation. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 128\u2013146. Springer, Heidelberg (1999)"},{"issue":"1","key":"14_CR19","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-71389-0_26","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Yoshida","year":"2007","unstructured":"Yoshida, N., Honda, K., Berge, M.: Logical reasoning for higher-order functions with local state. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 361\u2013377. Springer, Heidelberg (2007)"}],"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-642-10672-9_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:33:14Z","timestamp":1606185194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10672-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642106712","9783642106729"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10672-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}