Logic of bunched implications

Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.

The deduction theorem of classical logic relates conjunction and implication:

Bunched logic has two versions of the deduction theorem:

${\displaystyle A*B}$ and ${\displaystyle B{-\!\!*}C}$ are forms of conjunction and implication that take resources into account (explained below). In addition to these connectives bunched logic has a formula, sometimes written I or emp, which is the unit of *. In the original version of bunched logic ${\displaystyle \wedge }$ and ${\displaystyle \Rightarrow }$ were the connectives from intuitionistic logic, while a boolean variant takes ${\displaystyle \wedge }$ and ${\displaystyle \Rightarrow }$ (and ${\displaystyle \neg }$) as from traditional boolean logic. Thus, bunched logic is compatible with constructive principles, but is in no way dependent on them.

...
Wikipedia