Relational Parametricity and Separation Logic

TL;DR

This paper introduces a new interpretation of separation logic for higher-type programming languages using Reynolds's relational parametricity, establishing a formal link between separation logic and data abstraction.

Contribution

It provides the first formal connection between separation logic and relational parametricity for higher-order languages.

Findings

Establishes a formal connection between separation logic and data abstraction.

Extends the interpretation of separation logic to higher types.

Bridges the gap between reasoning about shared mutable data and data abstraction.

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