We consider the classical (propositional) version, CBI, of
O’Hearn and Pym’s logic of bunched implications (BI) from a model-
and proof-theoretic perspective. We make two main contributions in this
paper. Firstly, we present a class of algebraic models for CBI which per-
mit the full range of classical multiplicative connectives to be modelled.
Our models can be seen as generalisations of Abelian groups, and in-
clude several computationally interesting models as concrete instances.
Secondly, we give a display calculus proof system for CBI that is an
instance of Belnap’s general display logic — hence cut-eliminating —
and demonstrate this system to be sound and complete with respect to
validity in our models. To achieve the latter, we first define a simple
extension of the usual sequent calculus for BI by axioms that directly
capture properties of our models, and show this extension to be sound
and complete (though not cut-eliminating). Soundness and completeness
of our display calculus then follows by establishing faithful translations
between the display calculus and this sequent calculus.