We wish to announce the availability of the following paper, at the URL given below. The logic of linear functors by Richard Blute, J.R.B. Cockett, and R.A.G. Seely It has been commonplace to base logics and type theories on categorical doctrines; with this paper we propose a more general paradigm, suggesting that logics and type theories may be based on functorial doctrines. This paradigm is very general - in particular, it subsumes all of usual categorical logic and type theory as degenerate cases. So as to be able to make precise claims, we illustrate this idea with a special case, developing the logic of linear functors with sufficient detail to see that this one doctrine is general enough to deal with basic linear modal logic and with the Abrusci-Ruet mixed non-commutative linear logic. We emphasise the case where the logic is based on a single functor, but it will be clear that one could also base it on a family of functors, which would allow one to deal with process logic as considered by Hennessy and Milner. The paper's abstract is given in full below. The paper may be found at http://www.math.mcgill.ca/rags/linear/lfl.ps.gz> or go to R.A.G. Seely's home page http://www.math.mcgill.ca/rags/ and click on the appropriate link. ......................................................... The logic of linear functors by Richard Blute, J.R.B. Cockett, and R.A.G. Seely ABSTRACT: This paper describes a family of logics whose categorical semantics is based on functors with structure rather than on categories with structure. This allows the consideration of logics which contain possibly distinct logical subsystems whose interactions are mediated by functorial mappings. For example, within one unified framework, we shall be able to handle logics as diverse as modal logic, ordinary linear logic, and the "noncommutative logic" of Abrusci and Ruet, a variant of linear logic which has both commutative and noncommutative connectives. Although this paper will not consider in depth the categorical basis of this approach to logic, preferring instead to emphasize the syntactic novelties that it generates in the logic, we shall focus on the particular case when the logics are based on a linear functor, to give a definite presentation of these ideas. However, it will be clear that this approach to logic has considerable generality. There have been several individual attempts to develop logics with distinct but related subsystems of connectives, such as the Abrusci--Ruet noncommutative logic and the bunch logic of O'Hearn and Pym; generally these are presented in terms of "bunching" the formulas in the sequents of the logics via different "punctuation". The present functor logic, by contrast, uses a system of "formula blocks", which represent the functorial action and which give finer control over what logical features may be displayed. By displaying a family of functor logics, we illustrate how different logical systems can be developed along these lines, logics which are primarily distinguished by the degree to which they permit nesting of formula blocks. Our examples will include a basic logic where there is essentially no nesting, a system of linear modal logic, which allows nesting, but has only one system of connectives, and the Abrusci--Ruet logic, where nesting is virtually unrestricted and there are two subsystems of connectives. We finish by showing how to translate between the ``bunch'' style of logic and our ``formula block'' or functor logic using the Abrusci--Ruet noncommutative logic as an example. ================== R.A.G. Seely <rags@math.mcgill.ca> <http://www.math.mcgill.ca/rags>