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

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Tidsskriftartikel › Forskning › peer review

Abstract

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

Originalsprog	Engelsk
Tidsskrift	Logical Methods in Computer Science
Vol/bind	4
Udgave nummer	2
Sider (fra-til)	1-27
Antal sider	27
ISSN	1860-5974
DOI	https://doi.org/10.2168/LMCS-4(2:6)2008
Status	Udgivet - 2008

Adgang til dokumentet

10.2168/LMCS-4(2:6)2008

Citationsformater

@article{ce869fc0896e11dd8006000ea68e967b,

title = "Relational Parametricity and Separation Logic",

abstract = "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",

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

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

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 -