  The logic of Bunched Implications (BI) freely combines additive and
multiplicative connectives, including implications; however, despite its
well-studied proof theory, proof-search in BI has always been a difficult
problem. The focusing principle is a restriction of the proof-search space that
can capture various goal-directed proof-search procedures. In this paper, we
show that focused proof-search is complete for BI by first reformulating the
traditional bunched sequent calculus using the simpler data-structure of nested
sequents, following with a polarised and focused variant that we show is sound
and complete via a cut-elimination argument. This establishes an operational
semantics for focused proof-search in the logic of Bunched Implications.
