Relational Parametricity and Separation Logic

Lars Birkedal, Hongseok Yang

    Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review


    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
    Original languageEnglish
    JournalLogical Methods in Computer Science
    Issue number2
    Pages (from-to)1-27
    Number of pages27
    Publication statusPublished - 2008

    Cite this