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.
[2] The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic,[3] and in systems modelling, where it provides a way to decompose the resources used by components of a system.
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 *.
advanced by Pym, where the forcing relation means 'A holds of resource r'.
The semantics is analogous to Kripke's semantics of intuitionistic or modal logic, but where the elements of the model are regarded as resources that can be composed and decomposed, rather than as possible worlds that are accessible from one another.
(or of negation) is often rejected by relevantists in their bid to escape the `paradoxes of material implication', which are not a problem from the perspective of modelling resources and so not rejected by bunched logic.
These considerations are discussed in detail in an article on resource semantics by Pym, O'Hearn and Yang.
[7] The double version of the deduction theorem of bunched logic has a corresponding category-theoretic structure.
[8] Additionally, the implicational fragment of bunched logic has been given a game semantics.
The proof calculus of bunched logic differs from usual sequent calculi in having a tree-like context of hypotheses instead of a flat list-like structure.
is a finite rooted tree whose leaves are propositions and whose internal nodes are labelled with modes of composition corresponding to the two conjunctions.
The two combining operators, comma and semicolon, are used (for instance) in the introduction rules for the two implications.
[10] But the bunched structure can in a sense be derived from the categorical and algebraic semantics: to formulate an introduction rule for
James Brotherston has done further significant work on a unified proof theory for bunched logic and variants,[11] employing Belnap's notion of display logic.
[12] Galmiche, Méry, and Pym have provided a comprehensive treatment of bunched logic, including completeness and other meta-theory, based on labelled tableaux.
[13] In perhaps the first use of substructural type theory to control resources, John C. Reynolds showed how to use an affine type theory to control aliasing and other forms of interference in Algol-like programming languages.
[14] O'Hearn used bunched type theory to extend Reynolds' system by allowing interference and non-interference to be more flexibly mixed.
[2] This resolved open problems concerning recursion and jumps in Reynolds' system.
, but the preconditions and postconditions are formulae interpreted in a model of bunched logic.
Separation logic was used originally to prove properties of sequential programs, but then was extended to concurrency using a proof rule that divides the storage accessed by parallel threads.
[15] Later, the greater generality of the resource semantics was utilized: an abstract version of separation logic works for Hoare triples where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model.
[16] By suitable choice of commutative monoid, it was surprisingly found that the proofs rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding rely-guarantee and trace-based reasoning.
[19] Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP[4][5][6] in order to give a (modal) logic that characterizes, in the sense of Hennessy–Milner, the compositional structure of concurrent systems.
While direct and intuitively appealing, this choice leads to a specific technical problem: the Hennessy–Milner completeness theorem holds only for fragments of the modal logic that exclude the multiplicative implication and multiplicative modalities.
This problem is solved by basing resource-process calculus on a resource semantics in which resource elements are combined using two combinators, one corresponding to concurrent composition and one corresponding to choice.
[20] Cardelli, Caires, Gordon and others have investigated a series of logics of process calculi, where a conjunction is interpreted in terms of parallel composition.
[citation needed] Unlike the work of Pym et al. in SCRP, they do not distinguish between parallel composition of systems and composition of resources accessed by the systems.
Although these logics give rise to instances of boolean bunched logic, they appear to have been arrived at independently, and in any case have significant additional structure in the way of modalities and binders.