Lars Birkedal ; Hongseok Yang - Relational Parametricity and Separation Logic

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

Authors: Lars Birkedal ; Hongseok Yang

    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.

    Volume: Volume 4, Issue 2
    Published on: May 15, 2008
    Imported on: September 21, 2007
    Keywords: Computer Science - Logic in Computer Science,F.3,D.3


    Is referenced by
    Dependent Type Theory for Verification of Information Flow and Access Control Policies
    • 1 ScholeXplorer


    Consultation statistics

    This page has been seen 883 times.
    This article's PDF has been downloaded 285 times.