Internal Calculi for Separation Logics
Logic in Computer Science
2019-10-14 v1
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.
Keywords
Cite
@article{arxiv.1910.05016,
title = {Internal Calculi for Separation Logics},
author = {Stéphane Demri and Etienne Lozes and Alessio Mansutti},
journal= {arXiv preprint arXiv:1910.05016},
year = {2019}
}