Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2020.19
URN: urn:nbn:de:0030-drops-116625
URL: https://drops.dagstuhl.de/opus/volltexte/2020/11662/
Demri, Stéphane ; Lozes, Etienne ; Mansutti, Alessio
Internal Calculi for Separation Logics
| pdf-format: |
|
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 SL(∗, -*). 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.
BibTeX - Entry
@InProceedings{demri_et_al:LIPIcs:2020:11662,
author = {St{\'e}phane Demri and Etienne Lozes and Alessio Mansutti},
title = {{Internal Calculi for Separation Logics}},
booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
pages = {19:1--19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-132-0},
ISSN = {1868-8969},
year = {2020},
volume = {152},
editor = {Maribel Fern{\'a}ndez and Anca Muscholl},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/11662},
URN = {urn:nbn:de:0030-drops-116625},
doi = {10.4230/LIPIcs.CSL.2020.19},
annote = {Keywords: Separation logic, internal calculus, adjunct/quantifier elimination}
}
| Keywords: | Separation logic, internal calculus, adjunct/quantifier elimination | |
| Seminar: | 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) | |
| Issue date: | 2020 | |
| Date of publication: | 06.01.2020 |
