{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:29Z","timestamp":1775790689380,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425540","type":"print"},{"value":"9783540448020","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_1","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T04:15:38Z","timestamp":1180671338000},"page":"1-19","source":"Crossref","is-referenced-by-count":312,"title":["Local Reasoning about Programs that Alter Data Structures"],"prefix":"10.1007","author":[{"given":"Peter","family":"O\u2019Hearn","sequence":"first","affiliation":[]},{"given":"John","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"809","DOI":"10.1109\/32.469460","volume":"21","author":"A. Borgida","year":"1995","unstructured":"A. Borgida, J. Mylopoulos, and R. Reiter. On the frame problem in procedure specifications. IEEE Transactions of Software Engineering, 21:809\u2013838, 1995.","journal-title":"IEEE Transactions of Software Engineering"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"R. Bornat. Proving pointer programs in Hoare logic. Mathematics of Program Construction, 2000.","DOI":"10.1007\/10722010_8"},{"key":"1_CR3","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"R.M. Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, 7:23\u201350, 1972.","journal-title":"Machine Intelligence"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"C. Calcagno, S. Isthiaq, and P. W. O\u2019Hearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. Proceedings of the Second International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2000.","DOI":"10.1145\/351268.351291"},{"key":"1_CR5","first-page":"843","volume-title":"Handbook of Theoretical Computer Science","author":"P. Cousot","year":"1990","unstructured":"P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 843\u2013993. Elsevier, Amsterdam, and The MIT Press, Cambridge, Mass., 1990."},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"ECCOP\u201999-Object-Oriented Programming, 13th European Conference","author":"C. A. R. Hoare","year":"1999","unstructured":"C. A. R. Hoare and J. He. A trace model for pointers and objects. In Rachid Guerraoui, editor, ECCOP\u201999-Object-Oriented Programming, 13th European Conference, pages 1\u201317, 1999. Lecture Notes in Computer Science, Vol. 1628, Springer."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"S. Isthiaq and P.W. O\u2019Hearn. BI as an assertion language for mutable data structures. In Conference Record of the Twenty-Eighth Annual ACM Symposium on Principles of Programming Languages, pages 39\u201346, London, January 2001.","DOI":"10.1145\/360204.375719"},{"key":"1_CR8","volume-title":"Technical Report Reearch Report 160","author":"K. R. M. Leino","year":"2000","unstructured":"K. R. M. Leino and G. Nelson. Data abstraction and information hiding. Technical Report Reearch Report 160, Compaq Systems Research Center, Palo Alto,CA, November 2000."},{"key":"1_CR9","first-page":"463","volume":"4","author":"J. McCarthy","year":"1969","unstructured":"J. McCarthy and P. Hayes. Some philosophical problems from the standpoint of artificial intelligence. Machine Intelligence, 4:463\u2013502, 1969.","journal-title":"Machine Intelligence"},{"key":"1_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Typed \u03bb-calculus and Applications","author":"P. W. O\u2019Hearn","year":"1999","unstructured":"P. W. O\u2019Hearn. Resource interpretations, bunched implications and the \u03b1\u03bb-calculus. In Typed \u03bb-calculus and Applications, J-Y Girard editor, L\u2019Aquila, Italy, April 1999. Lecture Notes in Computer Science 1581."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"P. W. O\u2019Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215\u2013244, June 99.","DOI":"10.2307\/421090"},{"issue":"1","key":"1_CR12","first-page":"267","volume":"47","author":"P. W. O\u2019Hearn","year":"2000","unstructured":"P. W. O\u2019Hearn and J. C. Reynolds. From Algol to polymorphic linear lambda-calculus. J. ACM, 47(1):267\u2013223, January 2000.","journal-title":"J. ACM"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"P. W. O\u2019Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3):658\u2013709, May 1995. Also in [14], vol 2, pages 109\u2013164.","DOI":"10.1145\/210346.210425"},{"key":"1_CR14","volume-title":"Algol-like Languages","year":"1997","unstructured":"P. W. O\u2019Hearn and R. D. Tennent, editors. Algol-like Languages. Two volumes, Birkhauser, Boston, 1997."},{"key":"1_CR15","series-title":"Ph.D. thesis","volume-title":"A Category-Theoretic Approach to the Semantics of Programming Languages","author":"F. J. Oles","year":"1982","unstructured":"F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. Ph.D. thesis, Syracuse University, Syracuse, N.Y., 1982."},{"key":"1_CR16","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-1-4757-3851-3_1","volume-title":"Algol-like Languages","author":"F. J. Oles","year":"1997","unstructured":"F. J. Oles. Functor categories and store shapes. In O\u2019Hearn and Tennent [14], pages 3\u201312. Vol. 2."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"D. J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Monograph to appear, 2001.","DOI":"10.1007\/978-94-017-0091-7"},{"key":"1_CR18","first-page":"39","volume-title":"Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages","author":"J. C. Reynolds","year":"1978","unstructured":"J. C. Reynolds. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39\u201346, Tucson, Arizona, January 1978. ACM, New York. Also in [14], vol 1."},{"key":"1_CR19","first-page":"345","volume-title":"Algorithmic Languages","author":"J. C. Reynolds","year":"1981","unstructured":"J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345\u2013372, Amsterdam, October 1981. North-Holland, Amsterdam. Also in [14], vol 1, pages 67\u201388."},{"key":"1_CR20","first-page":"303","volume-title":"Millennial Perspectives in Computer Science","author":"J. C. Reynolds","year":"2000","unstructured":"J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Jim Davies, Bill Roscoe, and Jim Woodcock, editors, Millennial Perspectives in Computer Science, pages 303\u2013321, Houndsmill, Hampshire, 2000. Palgrave."},{"key":"1_CR21","unstructured":"J. C. Reynolds. Lectures on reasoning about shared mutable data structure. IFIP Working Group 2.3 School\/Seminar on State-of-the-Art Program Design Using Logic. Tandil, Argentina, September 2000."},{"key":"1_CR22","unstructured":"M. Shanahan. Solving the Frame Problem: A Mathematical Investigation of the Common Sense Law of Inertia. MIT Press, 1997."},{"key":"1_CR23","unstructured":"H. Yang. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. Manuscript, October 2000."},{"key":"1_CR24","series-title":"Ph.D. thesis","volume-title":"Local Reasoning for Stateful Programs","author":"H. Yang","year":"2001","unstructured":"H. Yang. Local Reasoning for Stateful Programs. Ph.D. thesis, University of Illinois, Urbana-Champaign, Illinois, USA, 2001 (expected)."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:21:01Z","timestamp":1556464861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}