{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T17:40:23Z","timestamp":1740937223964,"version":"3.38.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["New Gener. Comput."],"published-print":{"date-parts":[[2011,1]]},"DOI":"10.1007\/s00354-010-0097-5","type":"journal-article","created":{"date-parts":[[2011,2,16]],"date-time":"2011-02-16T11:13:40Z","timestamp":1297854820000},"page":"3-29","source":"Crossref","is-referenced-by-count":1,"title":["Weak Updates and Separation Logic"],"prefix":"10.1007","volume":"29","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","published-online":{"date-parts":[[2011,2,16]]},"reference":[{"key":"97_CR1","unstructured":"Ahmed, A. J., \u201cSemantics of Types for Mutable State,\u201d Ph. D. thesis, Princeton University, 2004."},{"issue":"5","key":"97_CR2","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A. W. Appel","year":"2001","unstructured":"Appel, A. W. and McAllester, D., \u201cAn indexed model of recursive types for foundational proof-carrying code,\u201d ACM Trans. on Prog. Lang. and Sys., 23, 5, pp. 657-683, 2001.","journal-title":"ACM Trans. on Prog. Lang. and Sys."},{"key":"97_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A. W., Mellies, P.-A., Richards, C. D. and Vouillon, J., \u201cA very modal model of a modern, major, general type system,\u201d in Proc. of 34th ACM Symp. on Principles of Prog. Lang., ACM Press, pp. 109-122, Jan. 2007.","DOI":"10.1145\/1190215.1190235"},{"key":"97_CR4","doi-asserted-by":"crossref","unstructured":"Birkedal, L., St\u00f8vring, K. and Thamsborg, J., \u201cRealizability semantics of parametric polymorphism, references, and recursive types,\u201d in FoSSaCS, Springer-Verlag, pp. 456-470, April 2009.","DOI":"10.1007\/978-3-642-00596-1_32"},{"key":"97_CR5","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P. and Parkinson, M., \u201cPermission accounting in separation logic,\u201d in Proc. 32nd ACM Symp. on Principles of Prog. Lang., pp. 259-270, 2005.","DOI":"10.1145\/1047659.1040327"},{"issue":"4","key":"97_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1377492.1377493","volume":"30","author":"M. Furr","year":"2008","unstructured":"Furr, M. and Foster, J. S., \u201cChecking type safety of foreign function calls,\u201d ACM Trans. Program. Lang. Syst., 30, 4, pp. 1-63, 2008.","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"97_CR7","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0020-0190(95)00178-6","volume":"57","author":"R. Harper","year":"1996","unstructured":"Harper, R., \u201cA simplified account of polymorphic references,\u201d Information Processing Letters, 57, 1, pp. 15-16, 1996.","journal-title":"Information Processing Letters"},{"key":"97_CR8","doi-asserted-by":"crossref","unstructured":"Hoare, C. A. R., \u201cAn axiomatic basis for computer programming,\u201d Commun. ACM, 12, 10, pp. 578-580, October 1969.","DOI":"10.1145\/363235.363259"},{"key":"97_CR9","unstructured":"Honda, K., Yoshida, N. and Berger, M., \u201cAn observationally complete program logic for imperative higher-order frame rules,\u201d in Proc. 20th IEEE Symposium on Logic in Computer Science, pp. 270-279, June 2005."},{"key":"97_CR10","unstructured":"Krishnaswami, N., Birkedal, L., Aldrich, J. and Reynolds, J., \u201cIdealized ML and its separation logic,\u201d Unpublished manuscript, July 2007."},{"key":"97_CR11","doi-asserted-by":"crossref","unstructured":"Matthews, J. and Findler, R. B., \u201cOperational semantics for multi-language programs,\u201d in Proc. 34th ACM Symp. on Principles of Prog. Lang., pp. 3-10, 2007.","DOI":"10.1145\/1190216.1190220"},{"key":"97_CR12","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P. W., Reynolds, J. C. and Yang, H., \u201cLocal reasoning about programs that alter data structures,\u201d in Computer Science Logic, pp. 1-19, 2001.","DOI":"10.1007\/3-540-44802-0_1"},{"key":"97_CR13","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P. W., Yang, H. and Reynolds, J. C., \u201cSeparation and information hiding,\u201d in Proc. 31th ACM Symp. on Principles of Prog. Lang., pp. 268-280, Venice, Italy, Jan. 2004.","DOI":"10.1145\/982962.964024"},{"key":"97_CR14","unstructured":"Parkinson, M., \u201cLocal reasoning for Java,\u201d Ph.D. thesis, Tech Report UCAM-CL-TR-654, University of Cambridge Computer Laboratory, Oxford, Nov. 2005."},{"key":"97_CR15","doi-asserted-by":"crossref","unstructured":"Pottier, F., \u201cHiding local state in direct style: a higher-order anti-frame rule,\u201d in Proc. 23rd IEEE Symposium on Logic in Computer Science, pp. 331-340, June 2008.","DOI":"10.1109\/LICS.2008.16"},{"key":"97_CR16","doi-asserted-by":"crossref","unstructured":"Reus, B. and Schwinghammer, J., \u201cSeparation logic for higher-order store,\u201d in 20th International Workshop on Computer Science Logic (CSL), pp. 575-590, 2006.","DOI":"10.1007\/11874683_38"},{"key":"97_CR17","doi-asserted-by":"crossref","unstructured":"Reynolds, J. C., \u201cSeparation logic: A logic for shared mutable data structures,\u201d in Proc. 17th IEEE Symposium on Logic in Computer Science, pp. 55-74, July 2002.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"97_CR18","unstructured":"Tan, G. and Croft, J., \u201cAn empirical security study of the native code in the JDK,\u201d in 17th Usenix Security Symposium, pp. 365-377, 2008."},{"key":"97_CR19","doi-asserted-by":"crossref","unstructured":"Tan, G., Shao, Z., Feng, X. and Cai, H., \u201cWeak updates and separation logic,\u201d in Proc. of the 7th Asian Symposium on Programming Languages and Systems (APLAS \u201909), pp. 178-193, 2009.","DOI":"10.1007\/978-3-642-10672-9_14"},{"issue":"1","key":"97_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M. Tofte","year":"1990","unstructured":"Tofte, M., \u201cType inference for polymorphic references,\u201d Inf. and Comp., 89, 1, pp. 1-34, 1990.","journal-title":"Inf. and Comp."},{"issue":"2","key":"97_CR21","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M. Tofte","year":"1997","unstructured":"Tofte, M. and Talpin, J.-P., \u201cRegion-based memory management,\u201d Information and Computation, 132, 2, pp. 109-176, 1997.","journal-title":"Information and Computation"},{"key":"97_CR22","doi-asserted-by":"crossref","unstructured":"Trifonov, V. and Shao, Z., \u201cSafe and principled language interoperation,\u201d in 8th European Symposium on Programming (ESOP), pp. 128-146, 1999.","DOI":"10.1007\/3-540-49099-X_9"},{"key":"97_CR23","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V. and Parkinson, M. J., \u201cA marriage of rely\/guarantee and separation logic,\u201d in CONCUR, pp. 256-271, 2007.","DOI":"10.1007\/978-3-540-74407-8_18"},{"issue":"1","key":"97_CR24","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A. K. Wright","year":"1994","unstructured":"Wright, A. K. and Felleisen, M., \u201cA syntactic approach to type soundness,\u201d Information and Computation, 115, 1, pp. 38-94, 1994.","journal-title":"Information and Computation"},{"key":"97_CR25","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Honda, K. and Berge, M., \u201cLogical reasoning for higher-order functions with local state,\u201d in FoSSaCS (Seidl, H. ed.), pp. 361-377, March 2007.","DOI":"10.1007\/978-3-540-71389-0_26"}],"container-title":["New Generation Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-010-0097-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00354-010-0097-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-010-0097-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T17:15:22Z","timestamp":1740935722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00354-010-0097-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["97"],"URL":"https:\/\/doi.org\/10.1007\/s00354-010-0097-5","relation":{},"ISSN":["0288-3635","1882-7055"],"issn-type":[{"type":"print","value":"0288-3635"},{"type":"electronic","value":"1882-7055"}],"subject":[],"published":{"date-parts":[[2011,1]]}}}