Birkedal, Lars and Yang, Hongseok - Relational Parametricity and Separation Logic

lmcs:825 - Logical Methods in Computer Science, May 15, 2008, Volume 4, Issue 2
Relational Parametricity and Separation Logic

Authors: Birkedal, Lars and Yang, Hongseok

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.


Source : oai:arXiv.org:0805.0783
DOI : 10.2168/LMCS-4(2:6)2008
Volume: Volume 4, Issue 2
Published on: May 15, 2008
Submitted on: September 21, 2007
Keywords: Computer Science - Logic in Computer Science,F.3,D.3


Share

Consultation statistics

This page has been seen 72 times.
This article's PDF has been downloaded 13 times.