Bringing order to the separation logic jungle

Qinxiang Cao, Santiago Cuellar, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

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

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 15th Asian Symposium, APLAS 2017, Proceedings
EditorsBor-Yuh Evan Chang
PublisherSpringer Verlag
Pages190-211
Number of pages22
ISBN (Print)9783319712369
DOIs
StatePublished - Jan 1 2017
Event15th Asian Symposium on Programming Languages and Systems, APLAS 2017 - Suzhou, China
Duration: Nov 27 2017Nov 29 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10695 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other15th Asian Symposium on Programming Languages and Systems, APLAS 2017
CountryChina
CitySuzhou
Period11/27/1711/29/17

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Keywords

  • Order
  • Separation algebra
  • Separation logic

Fingerprint Dive into the research topics of 'Bringing order to the separation logic jungle'. Together they form a unique fingerprint.

Cite this