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.
An extended abstract of this paper was presented at the FOSSACS 2007 conference @cite_3 . This paper includes proofs that were missing in the conference version, and describes a general mathematical construction that lies behind our parametric model of separation logic. We also include a new example that illustrates the subtleties of the problems and results.
@cite_3
1511487092
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.