Relational Parametricity and Separation Logic
Logic in Computer Science
2015-07-01 v2
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.
Cite
@article{arxiv.0805.0783,
title = {Relational Parametricity and Separation Logic},
author = {Lars Birkedal and Hongseok Yang},
journal= {arXiv preprint arXiv:0805.0783},
year = {2015}
}