Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store
Polzer M, Goncharov S (2020)
Publication Type: Conference contribution
Publication year: 2020
Journal
Publisher: Springer
Book Volume: 12077 LNCS
Pages Range: 542-561
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Dublin
ISBN: 9783030452308
DOI: 10.1007/978-3-030-45231-5_28
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.
Authors with CRIS profile
Miriam Polzer
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Sergey Goncharov
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Related research project(s)
How to cite
APA:
Polzer, M., & Goncharov, S. (2020). Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store. In Jean Goubault-Larrecq, Barbara König (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 542-561). Dublin, IE: Springer.
MLA:
Polzer, Miriam, and Sergey Goncharov. "Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store." Proceedings of the 23rd International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin Ed. Jean Goubault-Larrecq, Barbara König, Springer, 2020. 542-561.
BibTeX: Download