Bunched Implications

Origin. O'Hearn and Pym introduced bunched implications (BI, 1999). Combines intuitionistic logic with linear/resource logic. Two conjunctions: additive (∧) and multiplicative (*). Foundation for separation logic. Substructural logic with resource sensitivity.

Models. Resources that split and combine. Intuitionistic logic: truth persists, premises can be reused. Linear logic: use each premise exactly once. BI: have both — some resources are reusable, some are consumable. Models heap memory: disjoint combination (*) and sharing (∧).

Formalism.

BI syntax: φ ::= p | ⊤ | ⊥ | I | φ ∧ ψ | φ ∨ ψ | φ → ψ | φ * ψ | φ —* ψ

Two conjunctions:

• φ ∧ ψ: additive (intuitionistic) — shared resources
• φ * ψ: multiplicative — disjoint resources

Two implications:

• φ → ψ: intuitionistic implication — reusable
• φ —* ψ: multiplicative implication (magic wand) — resource-consuming

Units:

• ⊤: additive truth (always available)
• I: multiplicative unit (empty resource)

Kripke resource semantics: Frame: (W, ≤, ∘, e) where:

• W: resource worlds
• ≤: resource extension (intuitionistic)
• ∘: W × W → W resource combination (monoidal)
• e: unit element

w ⊨ φ * ψ iff ∃w₁, w₂. w = w₁ ∘ w₂ and w₁ ⊨ φ and w₂ ⊨ ψ w ⊨ φ —* ψ iff ∀w'. w ∘ w' defined and w' ⊨ φ implies w ∘ w' ⊨ ψ

Boolean BI (BBI): Classical version: adds excluded middle for additive connectives. Used in separation logic.

Symbols.

Metatheory. Decidability is the unsettled point. Boolean BI is undecidable — proved twice independently at LICS 2010, by Brotherston and Kanovich (Minsky machines; J. ACM 2014) and by Larchey-Wendling and Galmiche (phase semantics; ToCL 2013). Intuitionistic BI was believed decidable for a decade on the strength of a semantic argument (Galmiche, Méry, Pym) and a later syntactic one (Ramanayake 2016), but a LICS 2026 result encodes Wang tilings into BI's ternary relational semantics and concludes that BI is undecidable too; the earlier proofs have not been reconciled with it. No PSPACE bound was ever established in any case. Cut elimination holds for the sequent calculus over bunched contexts, and Brotherston's display calculus gives a display-style presentation with a general cut-elimination theorem. BI is sound and complete for Kripke resource frames — a partial commutative monoid ordered by resource extension — and the categorical models are bicartesian doubly closed categories, cartesian closed and symmetric monoidal closed on the same objects, obtained from presheaves over the monoid by Day convolution. Separation logic is Boolean BI instantiated at the monoid of finite partial heaps under disjoint union, so the frame rule is not an extra principle but soundness of the *-rules in that model.

Applies to. Separation logic foundation. Memory and resource verification. Concurrent resource reasoning. File system verification. Linear/affine type systems. Access control (RBAC). Information flow.

Limitations. Contexts are bunches — trees with two kinds of node — and the structural rules are available at the additive nodes only: a hypothesis combined multiplicatively can be neither weakened away nor contracted, and no rule moves a formula between the two kinds of node, so the additive and multiplicative layers do not interact except through the frame semantics. Provability is undecidable for Boolean BI, and on the 2026 tiling reduction for intuitionistic BI as well, so no complete decision procedure exists and no complexity class bounds the problem. The separating implication is the source of the difficulty: an entailment with —* in the antecedent quantifies over all extensions of the current resource, which is what the undecidability proofs exploit, and it is why practical separation-logic tools work in fragments that omit it. BI itself fixes no model of resource — the heap laws and the frame rule are properties of a chosen partial commutative monoid, not theorems of BI — so the logic proves nothing about memory until a model is supplied, and different monoids validate different extensions.

© 2026 Lingenic LLC