A Modal Sequent Calculus for Propositional Separation Logic
Neelakantan R. Krishnaswami · 2008
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.