Title: An Algebraic Glimpse at Bunched Implications and Separation Logic,
Abstract: We overview the logic of Bunched Implications (BI) and Separation Logic (SL)
from a perspective inspired by Hiroakira Ono's algebraic approach to
substructural logics. We propose generalized BI algebras (GBI-algebras) as a
common framework for algebras arising via "declarative resource reading",
intuitionistic generalizations of relation algebras and arrow logics and the
distributive Lambek calculus with intuitionistic implication. Apart from
existing models of BI (in particular, heap models and effect algebras), we also
cover models arising from weakening relations, formal languages or more
fine-grained treatment of labelled trees and semistructured data. After briefly
discussing the lattice of subvarieties of GBI, we present a suitable duality
for GBI along the lines of Esakia and Priestley and an algebraic proof of cut
elimination in the setting of residuated frames of Galatos and Jipsen. We also
show how the algebraic approach allows generic results on decidability, both
positive and negative ones. In the final part of the paper, we gently introduce
the substructural audience to some theory behind state-of-art tools,
culminating with an algebraic and proof-theoretic presentation of
(bi-)abduction.