Relational Parametricity and Separation Logic

Lars Birkedal; Hongseok Yang

doi:10.2168/LMCS-4(2:6)2008

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 › Research › peer-review

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

Original language	English
Journal	Logical Methods in Computer Science
Volume	4
Issue number	2
Pages (from-to)	1-27
Number of pages	27
ISSN	1860-5974
DOIs	https://doi.org/10.2168/LMCS-4(2:6)2008
Publication status	Published - 2008

Keywords

Separation logic
Hoare logic
Shared mutable data
Relational parametricity
Data abstraction

Access to Document

10.2168/LMCS-4(2:6)2008

Cite this

@article{ce869fc0896e11dd8006000ea68e967b,

title = "Relational Parametricity and Separation Logic",

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{\textquoteright}s relational parametricity, and it provides a formal connection between separation logic and data abstraction",

keywords = "Separation logic, Hoare logic, Shared mutable data, Relational parametricity, Data abstraction, Separation logic, Hoare logic, Shared mutable data, Relational parametricity, Data abstraction",

author = "Lars Birkedal and Hongseok Yang",

note = "Paper id:: 10.2168/LMCS-4 (2:6) 2008",

year = "2008",

doi = "10.2168/LMCS-4(2:6)2008",

language = "English",

volume = "4",

pages = "1--27",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "International Federation for Computational Logic",

number = "2",

}

TY - JOUR

T1 - Relational Parametricity and Separation Logic

AU - Birkedal, Lars

AU - Yang, Hongseok

N1 - Paper id:: 10.2168/LMCS-4 (2:6) 2008

PY - 2008

Y1 - 2008

N2 - 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

AB - 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

KW - Separation logic

KW - Hoare logic

KW - Shared mutable data

KW - Relational parametricity

KW - Data abstraction

KW - Separation logic

KW - Hoare logic

KW - Shared mutable data

KW - Relational parametricity

KW - Data abstraction

U2 - 10.2168/LMCS-4(2:6)2008

DO - 10.2168/LMCS-4(2:6)2008

M3 - Journal article

SN - 1860-5974

VL - 4

SP - 1

EP - 27

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 2

ER -

Relational Parametricity and Separation Logic

Abstract

Keywords

Access to Document

Fingerprint

Cite this