Relational Parametricity and Separation Logic
- Lars Birkedal,
- Hongseok Yang
- Queen Mary University of London
Research Output:
Journal Article or Conference Article in Journal
Journal article
Peer-review
Open access
Publication Information
Output type
Research Output:
Journal Article or Conference Article in Journal
Journal article
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 1-27 (27 pages)Journal (Volume, Issue Number)
Logical Methods in Computer Science (Volume 4, Issue 2)Publication milestones
- Published - 2008
Publication status
Published - 2008
ISSN
1860-5974Publication IDs
- Scopus: 69549102206
Abstract
Separation logic is a recent extension of Hoare logic for reasoning about pro-
grams 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
grams 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
Publication metrics
PlumX, opens in new tab
Captures
4
Citations
15