2008/05/15 by Lars Birkedal, Hongseok Yang
Computer Science · #Axiomatic semantics #Bunched logic #Description logic #Dynamic logic (digital electronics) #Extension (predicate logic) #Formal Methods in Verification #Higher-order logic #Hoare logic #Logic programming #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Multimodal logic #Separation logic #cs.LO
paper · pdf · doi:10.2168/lmcs-4(2:6)2008
published as Logical Methods in Computer Science, Volume 4, Issue 2 (May 15, 2008) lmcs:825
arxiv created 2008/05/15 · openalex publication_date 2008/05/15 · arxiv updated 2015/07/01 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
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.