Relational Parametricity and Separation Logic

Lars Birkedal; Hongseok Yang

doi:10.2168/LMCS-4(2:6)2008

Lars Birkedal ; Hongseok Yang - Relational Parametricity and Separation Logic

lmcs:825 - Logical Methods in Computer Science, May 15, 2008, Volume 4, Issue 2 - https://doi.org/10.2168/LMCS-4(2:6)2008

Relational Parametricity and Separation LogicArticle

Authors: Lars Birkedal ; Hongseok Yang

Separation logic is a recent extension of Hoare logic for reasoning about programs with references to shared mutable data structures. In this paper, we provide a new interpretation of the logic for a programming language with higher types. Our interpretation is based on Reynolds's relational parametricity, and it provides a formal connection between separation logic and data abstraction.

https://doi.org/10.2168/LMCS-4(2:6)2008

Source: arXiv.org:0805.0783

Volume: Volume 4, Issue 2

Secondary volumes: Selected Papers of the 10th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2007)

Published on: May 15, 2008

Imported on: September 21, 2007

Keywords: Computer Science - Logic in Computer Science, F.3, D.3

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

12 Documents citing this article

Dan Frumin;Amin Timany;Lars Birkedal, 2024, Modular Denotational Semantics for Effects with Guarded Interaction Trees, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 332-361, 10.1145/3632854, https://doi.org/10.1145/3632854.

Anindya Banerjee;Ramana Nagasamudram;David A. Naumann;Mohammad Nikouei, 2022, A Relational Program Logic with Data Abstraction and Dynamic Framing, ACM Transactions on Programming Languages and Systems, 44, 4, pp. 1-136, 10.1145/3551497, https://doi.org/10.1145/3551497.

Aleksandar Nanevski;Anindya Banerjee;Deepak Garg, 2013, Dependent Type Theory for Verification of Information Flow and Access Control Policies, ACM Transactions on Programming Languages and Systems, 35, 2, pp. 1-41, 10.1145/2491522.2491523, https://doi.org/10.1145/2491522.2491523.

Anindya Banerjee;David A. Naumann, 2013, State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings, Lecture notes in computer science, pp. 319-365, 10.1007/978-3-642-36946-9_12.

Jonas B. Jensen;Nick Benton;Andrew Kennedy, 2013, High-level separation logic for low-level code, IT University Of Copenhagen (IT University of Copenhagen), pp. 301-314, 10.1145/2429069.2429105.

Jonas B. Jensen;Nick Benton;Andrew Kennedy, 2013, High-level separation logic for low-level code, ACM SIGPLAN Notices, 48, 1, pp. 301-314, 10.1145/2480359.2429105.

David A. Naumann;Augusto Sampaio;Leila Silva, 2012, Refactoring and representation independence for class hierarchies, Theoretical Computer Science, 433, pp. 60-97, 10.1016/j.tcs.2012.02.009.

Aleksandar Nanevski;Viktor Vafeiadis;Josh Berdine, 2010, Structuring the verification of heap-manipulating programs, ACM SIGPLAN Notices, 45, 1, pp. 261-274, 10.1145/1707801.1706331.

Derek Dreyer;Georg Neis;Andreas Rossberg;Lars Birkedal, 2010, A relational modal logic for higher-order stateful ADTs, ACM SIGPLAN Notices, 45, 1, pp. 185-198, 10.1145/1707801.1706323.

Ivana Filipović;Peter O’Hearn;Noah Torp-Smith;Hongseok Yang, 2009, Blaming the client: on data refinement in the presence of pointers, Formal Aspects of Computing, 22, 5, pp. 547-583, 10.1007/s00165-009-0125-8, https://doi.org/10.1007/s00165-009-0125-8.

Viorel Preoteasa, 2009, Frame rule for mutually recursive procedures manipulating pointers, Theoretical Computer Science, 410, 42, pp. 4216-4233, 10.1016/j.tcs.2009.05.016.

MATTHEW COLLINSON;DAVID PYM;EDMUND ROBINSON, 2008, Bunched polymorphism, Mathematical Structures in Computer Science, 18, 6, pp. 1091-1132, 10.1017/s0960129508007159.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3207 times.

This article's PDF has been downloaded 537 times.