Abstract
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 full ground store, in terms of a full ground store monad, to build a corresponding semantics of a higher order logic over the corresponding programs. Our main result is a construction of an (intuitionistic) BI-hyperdoctrine, 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 (heaplets) 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 monoid.
Sergey Goncharov acknowledges support by German Research Foundation (DFG) under project GO 2161/1-2.
Chapter PDF
Similar content being viewed by others
References
Samson Abramsky. Intensionality, definability and computation. In Alexandru Baltag and Sonja Smets, editors, Johan van Benthem on Logic and Information Dynamics, pages 121–142. Springer, 2014.
Bodil Biering, Lars Birkedal, and Noah Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst., 29(5), 2007.
Ales Bizjak and Lars Birkedal. On models of higher-order separation logic. Electr. Notes Theor. Comput. Sci., 336:57–78, 2018.
Cristiano Calcagno, Peter O’Hearn, and Richard Bornat. Program logic and equivalence in the presence of garbage collection. Theoretical Computer Science, 298(3):557–581, 2003. Foundations of Software Science and Computation Structures.
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.
Peter Johnstone. Sketches of an elephant: A topos theory compendium. Oxford logic guides. Oxford Univ. Press, New York, 2002.
Peter T Johnstone. Conditions related to De Morgan’s law. In Applications of sheaves, pages 479–491. Springer, 1979.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš 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.
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–12, 2017.
William Lawvere. Adjointness in foundations. Dialectica, 23(3-4):281–296, 1969.
Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. & Comp, 185:2003, 2002.
Saunders Mac Lane.Categories for the Working Mathematician. Springer, 1971.
Kenji Maillard and Paul-André Melliès. A fibrational account of local states. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, pages 402–413. IEEE Computer Society, 2015.
Peter O'Hearn and Robert D. Tennent. Semantics of local variables. Applications of categories in computer science, 177:217–238, 1992.
Frank Joseph Oles. A Category-theoretic Approach to the Semantics of Programming Languages. PhD thesis, Syracuse University, Syracuse, NY, USA, 1982.
Gordon Plotkin and John Power. Notions of computation determine monads. In FoSSaCS'02, volume 2303 of LNCS, pages 342–356. Springer, 2002.
Gordon Plotkin and John Power. Algebraic operations and generic effects. Appl. Cat. Struct., 11(1):69–94, 2003.
David J. Pym, Peter W. O'Hearn, and Hongseok Yang. Possible worlds and resources: the semantics of BI. Theor. Comput. Sci., 315:257–305, May 2004.
John Reynolds. The essence of ALGOL. In Peter W. O'Hearn and Robert D. Tennent, editors, ALGOL-like Languages, Volume 1, pages 67–88. Birkhauser Boston Inc., Cambridge, MA, USA, 1997.
John Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, pages 303–321. Palgrave, 2000.
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–74. IEEE Computer Society, 2002.
Alex Simpson. Category-theoretic structure for independence and conditional independence. Electr. Notes Theor. Comput. Sci., 336:281–297, 2018.
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–519, June 2013.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Polzer, M., Goncharov, S. (2020). Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_28
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)