Relational Parametricity and Separation Logic

Abstract. 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 separation logic and data abstraction.

• Type: Conference
• Year: 2007
• Where: FOSSACS
• Authors: Lars Birkedal, Hongseok Yang
• Keywords: Applied Computing, Connection Separation Logic, FOSSACS 2007, Hoare Logic, Separation Logic