We wish to announce the following paper made available for ftp on our WWW site.

Theory and Applications of Categories, Vol. 3, 1997, No. 5, pp. 85-131

Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories
J.R.B. Cockett and R.A.G. Seely

This note applies techniques we have developed to study coherence in monoidal categories with two tensors, corresponding to the tensor-par fragment of linear logic, to several new situations, including Hyland and de Paiva's Full Intuitionistic Linear Logic (FILL), and Lambek's Bilinear Logic (BILL). Note that the latter is a noncommutative logic; we also consider the noncommutative version of FILL. The essential difference between FILL and BILL lies in requiring that a certain tensorial strength be an isomorphism. In any FILL category, it is possible to isolate a full subcategory of objects (the ``nucleus'') for which this transformation is an isomorphism. In addition, we define and study the appropriate categorical structure underlying the MIX rule. For all these structures, we do not restrict consideration to the ``pure'' logic as we allow non-logical axioms. We define the appropriate notion of proof nets for these logics, and use them to describe coherence results for the corresponding categorical structures.

Theory and Applications of Categories, Vol. 3, 1997, No. 5, 85-131

We would draw your attention to the following "highlights":

The paper is available by ftp as a PS file or as a DVI file as well as on Robert Seely's WWW home page and the TAC home page.
For assistance with ftp, please contact rags@math.mcgill.ca.

Robin Cockett
Robert Seely