{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T08:02:26Z","timestamp":1750492946751},"publisher-location":"Berlin, Heidelberg","reference-count":22,"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_17","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T18:42:00Z","timestamp":1292870520000},"page":"233-247","source":"Crossref","is-referenced-by-count":28,"title":["BI Hyperdoctrines and Higher-Order Separation Logic"],"prefix":"10.1007","author":[{"given":"Bodil","family":"Biering","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noah","family":"Torp-Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Biering, B.: On the logic of bunched implications and its relation to separation logic. Master\u2019s thesis, University of Copenhagen (2004)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: Proceedings of the 31-st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), Venice, Italy, pp. 220\u2013231 (2004)","DOI":"10.1145\/964001.964020"},{"key":"17_CR3","unstructured":"Bornat, R.: Local reasoning, separation and aliasing. In: Proceedings of the Second Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE 2004), Venice, Italy (January 2004)"},{"key":"17_CR4","volume-title":"Proceedings of POPL 2005","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of POPL 2005, Long Beach, CA, USA, January 2005. ACM, New York (2005) Accepted for publication"},{"issue":"3","key":"17_CR5","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/S0304-3975(02)00868-X","volume":"298","author":"C. Calcagno","year":"2003","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Bornat, R.: Program logic and equivalence in the presence of garbage collection. Theoretical Computer Science\u00a0298(3), 557\u2013587 (2003)","journal-title":"Theoretical Computer Science"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001 (2001)","DOI":"10.1145\/360204.375719"},{"key":"17_CR7","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol.\u00a0141. North-Holland Publishing Co., Amsterdam (1999)"},{"issue":"3\/4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","volume":"23","author":"F.W. Lawvere","year":"1969","unstructured":"Lawvere, F.W.: Adjointness in foundations. Dialectica\u00a023(3\/4), 281\u2013296 (1969)","journal-title":"Dialectica"},{"key":"17_CR9","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., Yang, H., Reynolds, J.C.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"17_CR10","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding (work in progress). Extended version of [11] (2003)"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proceedings of the 31-st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), Venice, Italy, pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"issue":"2","key":"17_CR12","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05(2), 215\u2013244 (1999)","journal-title":"Bulletin of Symbolic Logic"},{"key":"17_CR13","volume-title":"Algebraic and Logical Structures Handbook of Logic in Computer Science, ch.\u00a02","author":"A.M. Pitts","year":"2000","unstructured":"Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Algebraic and Logical Structures Handbook of Logic in Computer Science, ch.\u00a02, vol.\u00a05. Oxford University Press, Oxford (2000)"},{"issue":"1","key":"17_CR14","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.tcs.2003.11.020","volume":"315","author":"D. Pym","year":"2004","unstructured":"Pym, D., O\u2019Hearn, P.W., Yang, H.: Possible worlds and resources: The semantics of BI. Theoretical Computer Science\u00a0315(1), 257\u2013305 (2004)","journal-title":"Theoretical Computer Science"},{"key":"17_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"D.J. Pym","year":"2002","unstructured":"Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"17_CR16","unstructured":"Pym, D.J.: Errata and remarks for the semantics and proof theory of the logic of bunched implications (2004), Available at \n                  \n                    http:\/\/www.cs.bath.ac.uk\/~pym\/BI-monograph-errata.pdf"},{"key":"17_CR17","unstructured":"Reynolds, J.C.: On extensions of separation logic. Private Communication"},{"key":"17_CR18","volume-title":"The Craft of Programming","author":"J.C. Reynolds","year":"1981","unstructured":"Reynolds, J.C.: The Craft of Programming. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"17_CR19","first-page":"303","volume-title":"Millennial Perspectives in Computer Science","author":"J.C. Reynolds","year":"2000","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, pp. 303\u2013321. Palgrave, Houndsmill, Hampshire (2000)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Seventeenth Annual IEEE symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"17_CR21","unstructured":"Yang, H.: Local Reasoning for Stateful Programs. PhD thesis, University of Illinois, Urbana-Champaign (2001)"},{"issue":"1","key":"17_CR22","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.scico.2004.01.007","volume":"50","author":"H. Yang","year":"2004","unstructured":"Yang, H., Reddy, U.: Correctness of data representations involving heap data structures. Science of Computer Programming\u00a050(1), 129\u2013160 (2004)","journal-title":"Science of Computer Programming"}],"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_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:44:53Z","timestamp":1620013493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31987-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540254355","9783540319870"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31987-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}