Journal article
A complete axiomisation for quantifier-free separation logic
- Abstract:
-
We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-style axiomatisation for quantifier-free separation logic. The calculus is divided in three parts: t...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Authors
Bibliographic Details
- Publisher:
- Logical Methods in Computer Science Publisher's website
- Journal:
- Logical Methods in Computer Science Journal website
- Volume:
- 17
- Issue:
- 3
- Publication date:
- 2021-08-10
- Acceptance date:
- 2021-07-19
- DOI:
- ISSN:
-
1860-5974
Item Description
- Language:
- English
- Keywords:
- Pubs id:
-
1190254
- Local pid:
- pubs:1190254
- Deposit date:
- 2021-08-10
Terms of use
- Copyright holder:
- Demri et al.
- Copyright date:
- 2021
- Rights statement:
- © S. Demri, E. Lozes, and A. Mansutti. This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany.
- Licence:
- CC Attribution (CC BY)
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record