Bunched logic

Bunched logic[1] 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 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.[4][5][6]

  1. ^ O'Hearn, Peter; Pym, David (1999). "The Logic of Bunched Implications" (PDF). Bulletin of Symbolic Logic. 5 (2): 215–244. CiteSeerX 10.1.1.27.4742. doi:10.2307/421090. JSTOR 421090. S2CID 2948552.
  2. ^ O'Hearn, Peter (2003). "On Bunched Typing" (PDF). Journal of Functional Programming. 13 (4): 747–796. doi:10.1017/S0956796802004495.
  3. ^ Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an assertion language for mutable data structures" (PDF). POPL. 28th (3): 14–26. CiteSeerX 10.1.1.11.4925. doi:10.1145/373243.375719.
  4. ^ Cite error: The named reference PymTofts2 was invoked but never defined (see the help page).
  5. ^ Cite error: The named reference :0 was invoked but never defined (see the help page).
  6. ^ Cite error: The named reference :1 was invoked but never defined (see the help page).