Bunched logic

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 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: and 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 and were the connectives from intuitionistic logic, while a boolean variant takes and (and ) as from traditional boolean logic. Thus, bunched logic is compatible with constructive principles, but is in no way dependent on them. The easiest way to understand these formulae is in terms of its truth-functional semantics. In this semantics a formula is true or false with respect to given resources. asserts that the resource at hand can be decomposed into resources that satisfy and . says that if we compose the resource at hand with additional resource that satisfies , then the combined resource satisfies . and have their familiar meanings. The foundation for this reading of formulae was provided by a forcing semantics advanced by Pym, where the forcing relation means A holds of resource r.