Journal article icon

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


Access Document


Files:
Publisher copy:
10.46298/lmcs-17(3:17)2021

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Publisher:
Logical Methods in Computer Science
Journal:
Logical Methods in Computer Science More from this journal
Volume:
17
Issue:
3
Publication date:
2021-08-10
Acceptance date:
2021-07-19
DOI:
ISSN:
1860-5974
Language:
English
Keywords:
Pubs id:
1190254
Local pid:
pubs:1190254
Deposit date:
2021-08-10

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP