Relational Parametricity and Separation Logic

Lars Birkedal, Hongseok Yang

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

    Abstrakt

    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.
    Udgivelsesdato: 2008
    OriginalsprogEngelsk
    TidsskriftLogical Methods in Computer Science
    Vol/bind4
    Udgave nummer2
    Sider (fra-til)1-27
    Antal sider27
    ISSN1860-5974
    DOI
    StatusUdgivet - 2008

    Citationsformater