A Modal Sequent Calculus for Propositional Separation Logic
The work
| Authors | Neelakantan R. Krishnaswami |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2008 |
| Citekey | krishnaswami2008modal |
Where it appeared
| Published in | IMLA 2008: 4th Workshop on Intuitionistic Modal Logic and Applications |
|---|
Identifiers
| OpenAlex | W2155156044 |
|---|
Access
| Landing page | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.1832 |
|---|---|
| Free full text | https://www.cl.cam.ac.uk/~nk480/separation-sequent.pdf |
Abstract
In this paper, we give a sequent calculus for separation logic. Unlike the logic of bunched implications, this calculus does not have a tree-shaped context – instead, we use labelled deduction to control when hypotheses can and cannot be used. We prove that cut-elimination holds for this calculus, and show that it is sound with respect to the provability semantics of separation logic.
A copy is held
pdf, 172.8 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-09-04 18:18 UTC |
Filed under
Cite it as
@inproceedings{krishnaswami2008modal,
title = {A Modal Sequent Calculus for Propositional Separation Logic},
author = {Neelakantan R. Krishnaswami},
year = {2008},
booktitle = {IMLA 2008: 4th Workshop on Intuitionistic Modal Logic and Applications},
}
This record lives at https://refs.drheap.org/krishnaswami2008modal/ and will keep doing so.