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 Logic

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
    Accepted on: June 25, 2015
    Submitted on: September 21, 2007
    Keywords: Computer Science - Logic in Computer Science,F.3,D.3

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1145/2491522.2491523
    • 10.1145/2491522.2491523
    • 10.1145/2491522.2491523
    Dependent Type Theory for Verification of Information Flow and Access Control Policies
    Nanevski, Aleksandar ; Banerjee, Anindya ; Garg, Deepak ;

    8 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 453 times.
    This article's PDF has been downloaded 259 times.