Lars Birkedal ; Hongseok Yang - Relational Parametricity and Separation Logic

lmcs:825 - Logical Methods in Computer Science, May 15, 2008, Volume 4, Issue 2 - https://doi.org/10.2168/LMCS-4(2:6)2008
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.

    https://doi.org/10.2168/LMCS-4(2:6)2008
    Source: arXiv.org:0805.0783
    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
    Licence: arXiv.org - Non-exclusive license to distribute

    Publications

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

    References

    Share and export

    Consultation statistics

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