{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:06Z","timestamp":1767929286105,"version":"3.49.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2007,8,2]],"date-time":"2007-08-02T00:00:00Z","timestamp":1186012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2007,8,2]]},"abstract":"<jats:p>\n            We present a precise correspondence between separation logic and a simple notion of\n            <jats:italic>predicate<\/jats:italic>\n            BI, extending the earlier correspondence given between part of separation logic and\n            <jats:italic>propositional<\/jats:italic>\n            BI. Moreover, we introduce the notion of a BI hyperdoctrine, show that it soundly models classical and intuitionistic first- and higher-order predicate BI, and use it to show that we may easily extend separation logic to\n            <jats:italic>higher-order<\/jats:italic>\n            . We also demonstrate that this extension is important for program proving, since it provides sound reasoning principles for data abstraction in the presence of aliasing.\n          <\/jats:p>","DOI":"10.1145\/1275497.1275499","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":55,"title":["BI-hyperdoctrines, higher-order separation logic, and abstraction"],"prefix":"10.1145","volume":"29","author":[{"given":"Bodil","family":"Biering","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Copenhagen S, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Copenhagen S, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noah","family":"Torp-Smith","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Copenhagen S, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,8,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101824"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_17"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Conference on Formal Techniques for Java-Like Programs.","author":"Barnett M."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the Conference on Mathematics of Program Construction (MPC).","author":"Barnett M."},{"key":"e_1_2_1_5_1","unstructured":"Biering B. 2004. On the logic of bunched implications and its relation to separation logic. M.S. thesis University of Copenhagen.  Biering B. 2004. On the logic of bunched implications and its relation to separation logic. M.S. thesis University of Copenhagen."},{"key":"e_1_2_1_6_1","unstructured":"Biering B. Birkedal L. Butz C. Hyland J. van Oosten J. and Streicher P. R. T. 2006. Notes on the dialectica topos. To appear.  Biering B. Birkedal L. Butz C. Hyland J. van Oosten J. and Streicher P. R. T. 2006. Notes on the dialectica topos. To appear."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.47"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964020"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the SPACE","author":"Bornat R.","year":"2004"},{"key":"e_1_2_1_11_1","unstructured":"Birkedal L. and Yang H. 2006. Relational parametricity and separation logic. To appear.  Birkedal L. and Yang H. 2006. Relational parametricity and separation logic. To appear."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_15_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"141","author":"Jacobs B.","year":"1999"},{"key":"e_1_2_1_16_1","unstructured":"Krishnaswami N. Birkedal L. Aldrich J. and Reynolds J. 2006. Idealized ML and its separation logic. To appear.  Krishnaswami N. Birkedal L. Aldrich J. and Reynolds J. 2006. Idealized ML and its separation logic. To appear."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Leavans G. 1988. Verifying object-oriented programs that use subtypes. Ph.D. thesis MIT. Published as MIT\/LCS\/TR-439 in February 1989.  Leavans G. 1988. Verifying object-oriented programs that use subtypes. Ph.D. thesis MIT. Published as MIT\/LCS\/TR-439 in February 1989.","DOI":"10.21236\/ADA209118"},{"key":"e_1_2_1_19_1","unstructured":"Leino K. 1995. Toward reliable modular programs. Ph.D. thesis California Institute of Technology.   Leino K. 1995. Toward reliable modular programs. Ph.D. thesis California Institute of Technology."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_9"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP).","author":"Leino K."},{"key":"e_1_2_1_22_1","unstructured":"Liskow B. and Guttag J. 1986. Abstraction and Specification in Program Development. MIT Press Cambridge MA.   Liskow B. and Guttag J. 1986. Abstraction and Specification in Program Development. MIT Press Cambridge MA."},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"MacLane S. and Moerdijk I. 1994. Sheaves in Geometry and Logic. Universitext. Springer New York. A first introduction to topos theory Corrected reprint of the 1992 edition.  MacLane S. and Moerdijk I. 1994. Sheaves in Geometry and Logic. Universitext. Springer New York. A first introduction to topos theory Corrected reprint of the 1992 edition.","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318606"},{"key":"e_1_2_1_25_1","volume-title":"Lecture Notes in Computer Science","volume":"2262","author":"M\u00fcller P.","year":"2002"},{"key":"e_1_2_1_26_1","volume-title":"Tech. Rep. TR--14-06","author":"Nanevski A.","year":"2006"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.035"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 15th International Conference on Concurrency Theory (CONCUR)","volume":"3170","author":"O'Hearn P. W.","year":"2004"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_2_1_30_1","unstructured":"O'Hearn P. W. Yang H. and Reynolds J. C. 2003. Separation and information hiding (work in progress). Extended version of O'Hearn et al. {2004}.  O'Hearn P. W. Yang H. and Reynolds J. C. 2003. Separation and information hiding (work in progress). Extended version of O'Hearn et al. {2004}."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_33_1","series-title":"Handbook of Logic in Computer Science","volume-title":"Algebraic and Logical Structures, S. Abramsky et al., eds","author":"Pitts A. M."},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Pym D. J. 2004. Errata and remarks for the semantics and proof theory of the logic of bunched implications. Addendum to Pym {2002}. http:\/\/www.cs.bath.ac.uk\/~pym\/.  Pym D. J. 2004. Errata and remarks for the semantics and proof theory of the logic of bunched implications. Addendum to Pym {2002}. http:\/\/www.cs.bath.ac.uk\/~pym\/.","DOI":"10.1007\/978-94-017-0091-7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0091-7"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_38_1","unstructured":"Silberschatz A. and Galvin P. 1998. Operating Systems Concepts 5th ed. World Student Series. Addison-Wesley Reading MA.   Silberschatz A. and Galvin P. 1998. Operating Systems Concepts 5th ed. World Student Series. Addison-Wesley Reading MA."},{"key":"e_1_2_1_39_1","unstructured":"Yang H. 2001. Local reasoning for stateful programs. Ph.D. thesis University of Illinois Urbana-Champaign.   Yang H. 2001. Local reasoning for stateful programs. Ph.D. thesis University of Illinois Urbana-Champaign."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704850"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275499","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1275497.1275499","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:30Z","timestamp":1750276830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275499"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8,2]]},"references-count":40,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,8,2]]}},"alternative-id":["10.1145\/1275497.1275499"],"URL":"https:\/\/doi.org\/10.1145\/1275497.1275499","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8,2]]},"assertion":[{"value":"2007-08-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}