Title: Modular Labelled Sequent Calculi for Abstract Separation Logics,
Abstract: Abstract separation logics are a family of extensions of Hoare logic for
reasoning about programs that manipulate resources such as memory locations.
These logics are "abstract" because they are independent of any particular
concrete resource model. Their assertion languages, called propositional
abstract separation logics (PASLs), extend the logic of (Boolean) Bunched
Implications (BBI) in various ways. In particular, these logics contain the
connectives $*$ and $-\!*$, denoting the composition and extension of resources
respectively.
This added expressive power comes at a price since the resulting logics are
all undecidable. Given their wide applicability, even a semi-decision procedure
for these logics is desirable. Although several PASLs and their relationships
with BBI are discussed in the literature, the proof theory and automated
reasoning for these logics were open problems solved by the conference version
of this paper, which developed a modular proof theory for various PASLs using
cut-free labelled sequent calculi. This paper non-trivially improves upon this
previous work by giving a general framework of calculi on which any new axiom
in the logic satisfying a certain form corresponds to an inference rule in our
framework, and the completeness proof is generalised to consider such axioms.
Our base calculus handles Calcagno et al.'s original logic of separation
algebras by adding sound rules for partial-determinism and cancellativity,
while preserving cut-elimination. We then show that many important properties
in separation logic, such as indivisible unit, disjointness, splittability, and
cross-split, can be expressed in our general axiom form. Thus our framework
offers inference rules and completeness for these properties for free. Finally,
we show how our calculi reduce to calculi with global label substitutions,
enabling more efficient implementation.