Bunched logic is a variety of substructural logic that, like linear logic, has classes of multiplicative and additive operators, but differs from usual proof calculi in having a tree-like context of hypotheses instead of a flat list-like structure; it is thus a calculus of deep inference. Sub-trees of the context tree are referred to as bunches; hence the name. The internal nodes in the context tree are labelled with the mode of composition — multiplicative or additive, with the following characteristics:

• Multiplicative composition denies the structural rules of weakening and contraction.
• Additive composition admits weakening and contraction of entire bunches.

Bunched logic extended with a semantic model of locations and store is known as separation logic . It has been used to define the logic of pointer-analysis in languages like Algol or C.

See also

• Linear logic

References

• O'Hearn P, On bunched typing, Journal of Functional Programming, 13(4), 747—796, 2003. (PDF)