R. Arisaka and S. Qin, LBI cut elimination proof with BI-Multi-Cut, TASE, pp.235-238, 2012.

J. Brotherston and C. Calcagno, Classical BI: a logic for reasoning about dualising resources, Proceedings of POPL-36, 2009.

K. Donnelly, T. Gibson, N. Krishnaswami, S. Magill, and S. Park, The Inverse Method for the Logic of Bunched Implications, LPAR, pp.466-480, 2004.
DOI : 10.1007/978-3-540-32275-7_31

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

D. Galmiche, D. Méry, and D. J. Pym, The semantics of BI and resource tableaux, Mathematical Structures in Computer Science, vol.15, issue.06, pp.1033-1088, 2005.
DOI : 10.1017/S0960129505004858
URL : https://hal.archives-ouvertes.fr/hal-00076735

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Harland and D. J. Pym, Resource-distribution via Boolean constraints, ACM Transactions on Computational Logic, vol.4, issue.1, pp.56-90, 2003.
DOI : 10.1145/601775.601778
URL : http://arxiv.org/abs/cs/0012018

N. Kamide, Temporal BI: Proof system, semantics and translations, Theoretical Computer Science, vol.492, pp.40-69, 2013.
DOI : 10.1016/j.tcs.2013.04.029

W. O. Peter and . Hearn, On bunched typing, Journal of Functional Programming, vol.13, issue.4, pp.747-796, 2003.

W. O. Peter, D. J. Hearn, and . Pym, The logic of bunched implications, Bulletin of Symbolic Logic, vol.5, issue.2, pp.215-244, 1999.

J. David and . Pym, The Semantics and Proof Theory of the Logic of Bunched Implications, 2002.

A. S. Troelstra and H. Schwichtenberg, Basic proof theory, 2000.
DOI : 10.1017/CBO9781139168717