5 citations · 8 across the 11 of their papers we have counts for
Showing 2013Show all
2 papers · 1 filter
cs.LO2013
Proof search for propositional abstract separation logics via labelled sequents
Zhe Hou, Ranald Clouston, Rajeev Gore +1
Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particu…
cs.LO2013
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
Zhe Hou, Alwen Tiu, Rajeev Gore
We present a labelled sequent calculus for Boolean BI, a classical variant of O'Hearn and Pym's logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cu…