Classical BI
      (A Logic for Reasoning About Dualising Resource)

                   James Brotherston
                Imperial College London


We show how to extend O'Hearn and Pym's logic of bunched
implications, BI, to classical BI (CBI), in which both the
additive and the multiplicative connectives behave classically.
Specifically, CBI is a non-conservative extension of
(propositional) boolean BI that includes multiplicative
versions of falsity, negation and disjunction.  We give an
algebraic semantics for CBI that leads us naturally to consider
resource models of CBI in which every resource has a unique
dual.  We also give a cut-eliminating proof system for CBI,
based on Belnap's display logic, which is sound and complete 
with respect to our semantics.

This is joint work with Cristiano Calcagno.