T. Braüner and V. de Paiva, “Cut-Elimination for Full Intuitionistic Linear Logic”, BRICS, vol. 3, no. 10, Jan. 1996.