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.

Symbol	Unicode	Name	Meaning
*	—	Separating conjunction	Disjoint combination
—*	—	Magic wand	Separating implication
∧	U+2227	Additive conjunction	Shared resources
→	U+2192	Implication	Intuitionistic
I	—	Emp	Empty resource
⊤	U+22A4	Top	Always true
∘	U+2218	Composition	Resource combination

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. Display calculus provides proof theory. Semantics: partial commutative monoids. Categorical: Day convolution on presheaves. Separation logic = BBI + memory 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. More complex than pure intuitionistic logic. Frame problem for —*. Tool support less than separation logic. Undecidability limits automation — certainly for Boolean BI, and on the 2026 result for intuitionistic BI as well. Choosing between * and ∧ requires care. Metatheory still being developed for extensions.