Bunched logic

From Wikipedia, the free encyclopedia

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.