Aarhus University Seal / Aarhus Universitets segl

Relational Parametricity and Separation Logic

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal 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
Pages (from-to)1-27
Number of pages27
Publication statusPublished - 2008
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 73743584