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 connectives of intuitionistic logic, BI is equipped with a separating conjunction and its corresponding implication , often referred to as a magic wand.
Please expand.
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].
Please expand.
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 and .
For more information see the 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.
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},
}
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},
}
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},
}