@inproceedings{e10f676142b643c9bb2837a13211da99,

title = "Bringing order to the separation logic jungle",

abstract = "Research results from so-called “classical” separation logics are not easily ported to so-called “intuitionistic” separation logics, and vice versa. Basic questions like, “Can the frame rule be proved independently of whether the programming language is garbage-collected?” “Can amortized resource analysis be ported from one separation logic to another?” should be straightforward. But they are not. Proofs done in a particular separation logic are difficult to generalize. We argue that this limitation is caused by incompatible semantics. For example, emp sometimes holds everywhere and sometimes only on units. In this paper, we introduce a unifying semantics and build a framework that allows to reason parametrically over all separation logics. Many separation algebras in the literature are accompanied, explicitly or implicitly, by a preorder. Our key insight is to axiomatize the interaction between the join relation and the preorder. We prove every separation logic to be sound and complete with respect to this unifying semantics. Further, our framework enables us to generalize the sound0.ness proofs for the frame rule and CSL. It also reveals a new world of meaningful intermediate separation logics between “intuitionistic” and “classical”.",

keywords = "Order, Separation algebra, Separation logic",

author = "Qinxiang Cao and Santiago Cuellar and Appel, {Andrew W.}",

note = "Funding Information: This research was supported in part by NSF Grant CCF-1521602. Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 15th Asian Symposium on Programming Languages and Systems, APLAS 2017 ; Conference date: 27-11-2017 Through 29-11-2017",

year = "2017",

doi = "10.1007/978-3-319-71237-6_10",

language = "English (US)",

isbn = "9783319712369",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "190--211",

editor = "Chang, {Bor-Yuh Evan}",

booktitle = "Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Proceedings",

address = "Germany",

}