Bi-intuitionistic Boolean Bunched Logic

We formulate and investigate a bi-intuitionistic extension, BiBBI, of the well known bunched logic Boolean BI, obtained by com-bining classical logic with full intuitionistic linear logic. Thus, in addition to the usual multiplicative conjunction ∗ (with its adjoint implication and unit), BiBBI also features an intuitionistic multi-plicative disjunction, ∗ ∨ (with its adjoint co-implication and unit). Intuitionism for the multiplicatives means that disjunction and con-junction are related by a weak distribution principle, rather than by De Morgan equivalence. We formulate a Kripke semantics for BiBBI in which the multi-plicatives are naturally read in terms of resource operations. Our main theoretical result is that validity according to this seman-tics coincides with provability, as given by a standard Hilbert-style proof system. From the program logic perspective, the main attraction of BiBBI compared to the earlier Classical BI is that its models in-clude the heap-like memory models of separation logic. In these models, the multiplicative disjunction can be interpreted as a prop-erty of intersection operations over heaps. Categories and Subject Descriptors F.3.1 [Logics and Mean