{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:04:43Z","timestamp":1743095083109,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452308"},{"type":"electronic","value":"9783030452315"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory. We capitalize on recent progress on categorical semantics of<jats:italic>full ground store<\/jats:italic>, in terms of a<jats:italic>full ground store monad<\/jats:italic>, to build a corresponding semantics of a higher order logic over the corresponding programs. Our main result is a construction of an<jats:italic>(intuitionistic) BI-hyperdoctrine<\/jats:italic>, which is arguably the semantic core of higher order logic over local store. Although we have made an extensive use of the existing generic tools, certain principled changes had to be made to enable the desired construction: while the original monad works over total heaps (to disable dangling pointers), our version involves partial heaps (<jats:italic>heaplets<\/jats:italic>) to enable compositional reasoning using separating conjunction. Another remarkable feature of our construction is that, in contrast to the existing generic approaches, our BI-algebra does not directly stem from an internal categorical partial commutative\u00a0monoid.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_28","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"542-561","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store"],"prefix":"10.1007","author":[{"given":"Miriam","family":"Polzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6924-8766","authenticated-orcid":false,"given":"Sergey","family":"Goncharov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Samson Abramsky. Intensionality, definability and computation. In Alexandru Baltag and Sonja Smets, editors, Johan van Benthem on Logic and Information Dynamics, pages 121\u2013142. Springer, 2014.","DOI":"10.1007\/978-3-319-06025-5_5"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Bodil Biering, Lars Birkedal, and Noah Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst., 29(5), 2007.","DOI":"10.1145\/1275497.1275499"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Ales Bizjak and Lars Birkedal. On models of higher-order separation logic. Electr. Notes Theor. Comput. Sci., 336:57\u201378, 2018.","DOI":"10.1016\/j.entcs.2018.03.016"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno, Peter O\u2019Hearn, and Richard Bornat. Program logic and equivalence in the presence of garbage collection. Theoretical Computer Science, 298(3):557\u2013581, 2003. Foundations of Software Science and Computation Structures.","DOI":"10.1016\/S0304-3975(02)00868-X"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono.Residuated Lattices: An Algebraic Glimpse at SubstructuralLogics, Volume 151. Elsevier Science, San Diego, CA, USA, 1st edition, 2007.","DOI":"10.1016\/S0049-237X(07)80005-X"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Peter Johnstone. Sketches of an elephant: A topos theory compendium. Oxford logic guides. Oxford Univ. Press, New York, 2002.","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Peter T Johnstone. Conditions related to De Morgan\u2019s law. In Applications of sheaves, pages 479\u2013491. Springer, 1979.","DOI":"10.1007\/BFb0061829"},{"key":"28_CR8","unstructured":"Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018."},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Ohad Kammar, Paul Blain Levy, Sean K. Moss, and Sam Staton. A monad for full ground reference cells. In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1\u201312, 2017.","DOI":"10.1109\/LICS.2017.8005109"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"William Lawvere. Adjointness in foundations. Dialectica, 23(3-4):281\u2013296, 1969.","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. & Comp, 185:2003, 2002.","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"28_CR12","unstructured":"Saunders Mac\u00a0Lane.Categories for the Working Mathematician. Springer, 1971."},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Kenji Maillard and Paul-Andr\u00e9 Melli\u00e8s. A fibrational account of local states. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, pages 402\u2013413. IEEE Computer Society, 2015.","DOI":"10.1109\/LICS.2015.45"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Peter O'Hearn and Robert D. Tennent. Semantics of local variables. Applications of categories in computer science, 177:217\u2013238, 1992.","DOI":"10.1017\/CBO9780511525902.013"},{"key":"28_CR15","unstructured":"Frank Joseph Oles. A Category-theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University, Syracuse, NY, USA, 1982."},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Gordon Plotkin and John Power. Notions of computation determine monads. In FoSSaCS'02, volume 2303 of LNCS, pages 342\u2013356. Springer, 2002.","DOI":"10.1007\/3-540-45931-6_24"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Gordon Plotkin and John Power. Algebraic operations and generic effects. Appl. Cat. Struct., 11(1):69\u201394, 2003.","DOI":"10.1023\/A:1023064908962"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"David J. Pym, Peter W. O'Hearn, and Hongseok Yang. Possible worlds and resources: the semantics of BI. Theor. Comput. Sci., 315:257\u2013305, May 2004.","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"John Reynolds. The essence of ALGOL. In Peter W. O'Hearn and Robert D. Tennent, editors, ALGOL-like Languages, Volume 1, pages 67\u201388. Birkhauser Boston Inc., Cambridge, MA, USA, 1997.","DOI":"10.1007\/978-1-4612-4118-8_4"},{"key":"28_CR20","unstructured":"John Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, pages 303\u2013321. Palgrave, 2000."},{"key":"28_CR21","unstructured":"John Reynolds. Separation logic: A logic for shared mutable data structures. In 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, pages 55\u201374. IEEE Computer Society, 2002."},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Alex Simpson. Category-theoretic structure for independence and conditional independence. Electr. Notes Theor. Comput. Sci., 336:281\u2013297, 2018.","DOI":"10.1016\/j.entcs.2018.03.028"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Sam Staton. Instances of computational effects: An algebraic perspective. In Proc. 28th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2013), pages 519\u2013519, June 2013.","DOI":"10.1109\/LICS.2013.58"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,4]],"date-time":"2024-08-04T06:08:47Z","timestamp":1722751727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}