The Logic of Bunched Implications (BI)

The logic of bunched implications (or BI) is a substructural logic that encodes various ideas of resource sharing. It forms the core of various program logics, such as separation logic.

In addition to the usual (\land \lor \to) connectives of intuitionistic logic, BI is equipped with a separating conjunction \ast and its corresponding implication \mathrel{-\mkern-6mu*}, often referred to as a magic wand.

Syntax

Please expand.

Cut elimination

Cut elimination for BI is fiddly. The original proof in Pym 2002, Chapter 6 has an error, which was fixed by Arisaka and Qin 2012.

A semantic proof of cut elimination, formalised in Coq, is given in Frumin 2022.

Kripke semantics

Please expand.

Categorical semantics

The categorical semantics of the proofs of BI is given by a bicartesian doubly closed category. This is category which is at once a bicartesian closed category (for the intuitionistic part) and also has a monoidal closed structure to interpret \ast and \mathrel{-\mkern-6mu*}.

For more information see the nLab page.

References

Wikipedia article
nLab page
The basic syntax and many results about BI can be found in the 1999 survey paper by O'Hearn and Pym:

O’Hearn, Peter W., and David J. Pym. ‘The Logic of Bunched Implications’. Bulletin of Symbolic Logic 5, no. 2 (1999): 215–44. https://doi.org/10.2307/421090.

@article{ohearn_1999,
	title = {The {Logic} of {Bunched} {Implications}},
	volume = {5},
	doi = {10.2307/421090},
	number = {2},
	journal = {Bulletin of Symbolic Logic},
	author = {O'Hearn, Peter W. and Pym, David J.},
	year = {1999},
	pages = {215--244},
}

Beware of PDFs that claim to be of this paper, such as this; the actual paper is much longer and far more technical.

A book-length treatment of the proof theory and semantics of BI is

Pym, David J. The Semantics and Proof Theory of the Logic of Bunched Implications. Vol. 26. Applied Logic Series. Dordrecht: Springer Netherlands, 2002. https://doi.org/10.1007/978-94-017-0091-7.

@book{pym_2002,
	address = {Dordrecht},
	series = {Applied {Logic} {Series}},
	title = {The {Semantics} and {Proof} {Theory} of the {Logic} of {Bunched} {Implications}},
	volume = {26},
	publisher = {Springer Netherlands},
	author = {Pym, David J.},
	editor = {Gabbay, Dov M. and Barwise, Jon},
	year = {2002},
	doi = {10.1007/978-94-017-0091-7},
}

A proof that fixes the error in the cut elimination proof of Pym 2002 can be found in

Arisaka, Ryuta, and Shengchao Qin. ‘LBI Cut Elimination Proof with BI-MultiCut’. In 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering, 235–38. Beijing, China: IEEE, 2012. https://doi.org/10.1109/TASE.2012.30.

@inproceedings{arisaka_lbi_2012,
	address = {Beijing, China},
	title = {{LBI} {Cut} {Elimination} {Proof} with {BI}-{MultiCut}},
	doi = {10.1109/TASE.2012.30},
	booktitle = {2012 {Sixth} {International} {Symposium} on {Theoretical} {Aspects} of {Software} {Engineering}},
	publisher = {IEEE},
	author = {Arisaka, Ryuta and Qin, Shengchao},
	month = jul,
	year = {2012},
	pages = {235--238},
}

A semantic proof of the cut elimination property for BI can be found in

Frumin, Dan. ‘Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq’. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, 291–306. Association for Computing Machinery, 2022. https://doi.org/10.1145/3497775.3503690.

@inproceedings{frumin_2022,
	title = {Semantic cut elimination for the logic of bunched implications, formalized in {Coq}},
	doi = {10.1145/3497775.3503690},
	booktitle = {Proceedings of the 11th {ACM} {SIGPLAN} {International} {Conference} on {Certified} {Programs} and {Proofs}},
	publisher = {Association for Computing Machinery},
	author = {Frumin, Dan},
	year = {2022},
	pages = {291--306},
}