A fresh look at separation algebras and share accounting

Robert Dockins, Aquinas Hobor, Andrew W. Appel

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

79 Scopus citations


Separation Algebras serve as models of Separation Logics; Share Accounting allows reasoning about concurrent-read/exclusive- write resources in Separation Logic. In designing a Concurrent Separation Logic and in mechanizing proofs of its soundness, we found previous axiomatizations of separation algebras and previous systems of share accounting to be useful but imperfect. We adjust the axioms of separation algebras; we demonstrate an operator calculus for constructing new separation algebras; we present a more powerful system of share accounting with a new, simple model; and we provide a reusable Coq development.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
Number of pages17
StatePublished - 2009
Event7th Asian Symposium on Programming Languages and Systems, APLAS 2009 - Seoul, Korea, Republic of
Duration: Dec 14 2009Dec 16 2009

Publication series

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


Other7th Asian Symposium on Programming Languages and Systems, APLAS 2009
Country/TerritoryKorea, Republic of

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'A fresh look at separation algebras and share accounting'. Together they form a unique fingerprint.

Cite this