Internal Calculi for Separation Logics

TL;DR

This paper introduces a novel internal Hilbert-style axiomatisation for quantifier-free separation logic, providing a foundational framework and analyzing its expressive power and computational complexity.

Contribution

It presents the first internal axiomatisation for quantifier-free separation logic and applies it to a new logic with separating conjunction, predicate ls, and guarded quantification.

Findings

Axiomatisation for quantifier-free separation logic

Introduction of a new separation logic with specific features

PSpace-completeness of the satisfiability problem

Abstract

We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic. We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem.