Paper Info
Title
Internal Calculi for Separation Logics.
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.
Year
DOI
Venue
2020
10.4230/LIPIcs.CSL.2020.19
CSL
Field
DocType
Citations 
Discrete mathematics,Computer science,Calculus
Conference
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Stéphane Demri100.34
Étienne Lozes212114.32
Alessio Mansutti3165.79