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

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

Bibliographic References

11 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, Lecture notes in computer science, State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings, pp. 319-365, 2013, 10.1007/978-3-642-36946-9_12.

Jonas B. Jensen;Nick Benton;Andrew Kennedy, Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, High-level separation logic for low-level code, 2013, Rome Italy, 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, https://doi.org/10.1016/j.tcs.2009.05.016.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1562 times.

This article's PDF has been downloaded 353 times.