{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T06:07:38Z","timestamp":1725602858532},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642229435"},{"type":"electronic","value":"9783642229442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22944-2_3","type":"book-chapter","created":{"date-parts":[[2011,8,25]],"date-time":"2011-08-25T05:45:59Z","timestamp":1314251159000},"page":"36-39","source":"Crossref","is-referenced-by-count":0,"title":["Abstract Local Reasoning for Program Modules"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Dinsdale-Young","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Wheelhouse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context Logic and tree update. In: POPL 2005, pp. 271\u2013282 (2005)","DOI":"10.1145\/1040305.1040328"},{"key":"3_CR2","first-page":"133","volume":"172","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Local reasoning about data update. ENTCS\u00a0172, 133\u2013175 (2007)","journal-title":"ENTCS"},{"key":"3_CR3","volume-title":"Data Refinement: Model-Oriented Proof Methods and Their Comparison","author":"W.-P. de Roever","year":"1999","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and Their Comparison. Cambridge University Press, Cambridge (1999)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-15057-9_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Gardner, P., Wheelhouse, M.: Abstraction and refinement for local reasoning. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 199\u2013215. Springer, Heidelberg (2010)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P., Torp-Smith, N., Yang, H.: Blaming the client: on data refinement in the presence of pointers. Formal Aspects of Computing (2009)","DOI":"10.1007\/s00165-009-0125-8"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Gardner, P.A., Smith, G.D., Wheelhouse, M.J., Zarfaty, U.D.: Local Hoare reasoning about DOM. In: PODS, pp. 261\u2013270 (2008)","DOI":"10.1145\/1376916.1376953"},{"issue":"10","key":"3_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 for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"4","key":"3_CR8","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf.\u00a01(4), 271\u2013281 (1972)","journal-title":"Acta Inf."},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-540-30538-5_35","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"I. Mijajlovi\u0107","year":"2004","unstructured":"Mijajlovi\u0107, I., Torp-Smith, N., O\u2019Hearn, P.W.: Refinement and separation contexts. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 421\u2013433. Springer, Heidelberg (2004)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. In: POPL, pp. 37\u201351 (1985)","DOI":"10.1145\/318593.318606"},{"key":"3_CR11","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., 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":"3_CR12","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"3_CR13","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513\u2013523 (1983)"}],"container-title":["Lecture Notes in Computer Science","Algebra and Coalgebra in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22944-2_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:09:54Z","timestamp":1606187394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22944-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642229435","9783642229442"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22944-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}