Editing Bunched logic (section)

== Applications ==

=== Interference control ===

In perhaps the first use of substructural type theory to control resources, [[John C. Reynolds]] showed how to use an [[Affine logic|affine]] type theory to control aliasing and other forms of interference in [[Algol]]-like programming languages.<ref>{{cite book|last1=Reynolds|first1=John|title=Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '78 |chapter=Syntactic control of interference |pages=39–46|doi=10.1145/512760.512766|year=1978|isbn=9781450373487|s2cid=18716926|doi-access=free}}</ref> O'Hearn used bunched type theory  to extend Reynolds' system by allowing interference and non-interference to be more flexibly mixed.<ref name = "OHearn02" /> This resolved open problems concerning recursion and jumps in Reynolds' system.

=== Separation logic ===

Separation logic is an extension of [[Hoare logic]] that facilitates reasoning about mutable data structures that use [[pointer (computer programming)|pointer]]s.  Following Hoare logic the formulae of separation logic are of the form
<math>\{Pre\} program \{Post\}</math>, but the preconditions and postconditions are formulae interpreted in a model of bunched logic.
The original version of the logic was based on models as follows:
* <math> Heaps = L \rightharpoonup_f V \qquad </math> (finite [[partial function]]s from locations to values)
* <math> h_0 \bullet h_1 = </math> union of heaps with disjoint domains, undefined when domains overlap.
It is the undefinedness of the composition on overlapping heaps that models the separation idea. This is a model of the boolean variant of bunched logic.

Separation logic was used originally to prove properties of sequential programs, but then was extended to concurrency using a proof rule
:<math> \frac{\{P_1\} C_1 \{Q_1\} \quad \{P_2\} C_2 \{Q_2\}}{\{P_1 * P_2\} C_1 \parallel C_2 \{Q_1 * Q_2\}}</math>
that divides the storage accessed by parallel threads.<ref>{{cite journal|last1=O'Hearn|first1=Peter|title=Resources, Concurrency and Local Reasoning|journal=Theoretical Computer Science|date=2007|volume=375|issue=1–3|pages=271–307|doi=10.1016/j.tcs.2006.12.035|url=http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concur04.pdf|doi-access=free}}</ref>

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.<ref>{{cite book |doi=10.1109/LICS.2007.30|chapter-url=http://www.cs.ox.ac.uk/people/hongseok.yang/paper/asl-short.pdf|isbn=978-0-7695-2908-0|citeseerx=10.1.1.66.6337|chapter=Local Action and Abstract Separation Logic|title=22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)|pages=366–378|year=2007|last1=Calcagno|first1=Cristiano|last2=O'Hearn|first2=Peter W.|last3=Yang|first3=Hongseok|s2cid=1044254}}</ref> 
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.<ref>{{cite journal|last1=Dinsdale-Young|first1=Thomas|last2=Birkedal|first2=Lars|last3=Gardner|first3=Philippa|last4=Parkinson|first4=Matthew|last5=Yang|first5=Hongseok|title=Views: Compositional Reasoning for Concurrent Programs|journal=Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages|volume=48|pages=287–300|date=2013|doi=10.1145/2480359.2429104|url=http://research.microsoft.com/pubs/180039/views.pdf}}</ref><ref>{{cite journal|last1=Sergey|first1=Ilya|last2=Nanevski|first2=Aleksandar|last3=Banerjee|first3=Anindya|title=Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity|journal=24th European Symposium on Programming|date=2015|url=http://ilyasergey.net/papers/histories-esop15.pdf|bibcode=2014arXiv1410.0306S|arxiv=1410.0306}}</ref>

Separation logic is the basis of a number of tools for automatic and semi-automatic reasoning about programs, and is used in the Infer program analyzer currently deployed at Facebook.<ref>{{cite web|last1=Calcagno|first1=Cristiano|last2=Distefano|first2=Dino|last3=O'Hearn|first3=Peter|title=Open-sourcing Facebook Infer: Identify bugs before you ship|url=https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/|date=2015-06-11}}</ref>

=== Resources and processes ===

Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP<ref name=PymTofts2>{{cite journal|last1=Pym|first1=David|last2=Tofts|first2=Chris|title=A Calculus and logic of resources and processes|journal=Formal Aspects of Computing|date=2006|volume=8|issue=4|pages=495–517|doi=10.1007/s00165-006-0018-z|s2cid=16623194|url=http://www0.cs.ucl.ac.uk/staff/D.Pym/pym-tofts-fac-preprint.pdf}}</ref><ref name=":0">{{Cite journal|title = Algebra and Logic for Resource-based Systems Modelling|last1 = Collinson|first1 = Matthew|journal = Mathematical Structures in Computer Science|doi = 10.1017/S0960129509990077|last2 = Pym|first2 = David|year = 2009|volume = 19|issue = 5|pages = 959–1027|citeseerx = 10.1.1.153.3899|s2cid = 14228156}}</ref><ref name=":1">{{Cite book|title = A Discipline of Mathematical Systems Modelling|last1 = Collinson|first1 = Matthew|publisher = College Publications|year = 2012|isbn = 978-1-904987-50-5|location = London|last2 = Monahan|first2 = Brian|last3 = Pym|first3 = David}}</ref> in order to give a (modal) logic that characterizes, in the sense of [[Matthew Hennessy|Hennessy]]–[[Robin Milner|Milner]], the compositional structure of concurrent systems.

SCRP is notable for interpreting <math> A * B </math> in terms of ''both'' parallel composition of systems and composition of their associated resources.
The semantic clause of SCRP's process logic that corresponds to separation logic's rule for concurrency asserts that a formula <math> A * B </math> is true in resource-process state <math> R </math>, <math> E </math> just in case there are decompositions of the resource <math>R = S \bullet T</math> and process 
<math>E</math> ~ <math>F \times G</math>, where ~ denotes [[bisimulation]], such that <math>A</math> is true in the resource-process state <math> S </math>, <math> F </math> and <math>B</math> is true in the resource-process state <math> T </math>, <math> G </math>; that is <math> R, E \models A </math> iff <math> S, F \models A </math> and <math> T, G \models B </math>.

The system SCRP<ref name="PymTofts2" /><ref name=":0" /><ref name=":1" /> is based directly on bunched logic's resource semantics; that is, on ordered monoids of resource elements. 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.<ref>{{Cite journal|title = A Calculus and Logic of Bunched Resources and Processes|last1 = Anderson|first1 = Gabrielle|date = 2015|journal = Theoretical Computer Science|volume = 614|pages = 63–96|doi = 10.1016/j.tcs.2015.11.035|last2 = Pym|first2 = David|doi-access = free}}</ref>

=== Spatial logics ===

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|date=October 2021}}
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.

Their logics are based on instances of the resource semantics that give rise to models of the boolean variant of bunched logic. 
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. Related logics have been proposed as well for modelling [[XML]] data.