On December 5, 1997, a small conference was held at McGill on the occasion of Jim Lambek's 75th birthday. Subsequently it was decided to publish two volumes of papers contributed in his honour to mark this occasion: this issue of Mathematical Structures in Computer Science is one of the volumes; the other is Volume 6 of the journal Theory and Applications of Categories. At the December 1997 conference, a brief biographical essay was presented by Michael Barr and appears in the TAC volume. However, we wish to make some further remarks here.

Jim completed his Ph.D. at McGill under Hans Zassenhaus in 1950, and has remained at McGill since then. But it is of interest to note that Jim wrote two theses: the second involved biquaternions in mathematical physics, and so foreshadows a significant feature of his career: Jim has consistently shown a remarkable range of interests, from physics to linguistics, from algebra to logic, from the history and philosophy of mathematics to the theory of computing science (although he never touches a computer, to this day!). Let us just review a small sample of his more than 100 published papers.

This paper presents a cut-elimination procedure for intuitionistic propositional logic in which cut is eliminated directly, without introducing the multiple-cut rule mix, and in which pushing cut above contraction is one of the reduction steps. The presentation of this procedure is preceded by an analysis of Gentzen's mix-elimination procedure, made in the perspective of permuting cut with contraction. We also show that in the absence of implication, pushing cut above contraction does not pose problems for directly eliminating cut.

We consider processes consisting of a category of states varying over a control category as prescribed by a unique factorisation lifting functor. After a brief analysis of the structure of general processes in this setting, we restrict attention to linearly-controlled ones. To this end, we introduce and study a notion of path-linearisable category in which any two paths of morphisms with equal composites can be linearised (or interleaved) in a canonical fashion. Our main result is that categories of linearly-controlled processes (viz., processes controlled by path-linearisable categories) are sheaf models.

Linear bicategories are a generalization of bicategories in which the one horizontal composition is replaced by two (linked) horizontal compositions. These compositions provide a semantic model for the tensor and par of linear logic: in particular, as composition is fundamentally non-commutative, they provide a suggestive source of models for non-commutative linear logic.

In a linear bicategory, the logical notion of complementation becomes a natural linear notion of adjunction. Just as ordinary adjoints are related to (Kan) extensions, these linear adjoints are related to the appropriate notion of linear extension.

There is also a stronger notion of complementation, which arises, for example, in cyclic linear logic. This sort of complementation is modelled by cyclic adjoints. This leads to the notion of a *ast;-linear bicategory and the coherence conditions that it must satisfy. Cyclic adjoints also give rise to linear monads: these are, essentially, the appropriate generalization (to the linear setting) of Frobenius algebras and the ambialgebras of Topological Quantum Field Theory.

A number of examples of linear bicategories arising from different sources are described, and a number of constructions that result in linear bicategories are indicated.

In another paper (Abramsky et al. 1999), we have developed Abramsky's analysis of Girard's Geometry of Interaction programme in detail. In this paper, our goal is to study the data ow based computational aspects of that analysis. We introduce unique decomposition categories that provide a suitable categorical framework for such computational analysis. The current study also serves to establish connections with the work on proof nets and paths by Girard and Danos and Regnier in this categorical setting. The latter goal is partially achieved here by the presentation of categorical models for dynamic algebras.

We prove a full completeness theorem for MLL without the Mix rule. This is done by interpreting a proof as a dinatural transformation in a *-autonomous category of reflexive topological abelian groups first studied by Barr, denoted [Rscr ][Tscr ][Ascr ]. In Section 2, we prove the unique interpretation theorem for a binary provable MLL-sequent. In Section 3, we prove a completeness theorem for binary sequents in MLL without the Mix rule, where we interpret formulas in the category [Rscr ][Tscr ][Ascr ]. The theorem is proved by investigating the concrete structure of [Rscr ][Tscr ][Ascr ], especially that arising from Pontrjagin's work on duality.

The representation of the inductively defined abstract data type for lists was left incomplete in Seldin (1997, Section 9). Here that representation is completed, and it is proved that all extra axioms needed are consistent. Among the innovations of this paper is a definition of cdr, whose definition was left for future work in Seldin (1997, Section 9). The results are then extended to other abstract data types – those of Berardi (1993). The method used to define cdr for lists is extended to obtain the definition of an inverse for each argument of each constructor of an abstract data type. These inverses are used to prove the injective property for the constructors. Also, Dedekind's method of defining the natural numbers is used to define a predicate associated with each abstract data type, and the use of this predicate makes it unnecessary to postulate the induction principle. The only axioms left to be proved are those asserting the disjointness of the co-domains of different constructors, and it is shown that those axioms can be proved consistent.

Non-commutative logic, which is a unification of commutative linear logic and cyclic linear logic, is extended to all linear connectives: additives, exponentials and constants. We give two equivalent versions of the sequent calculus (directly with the structure of order varieties, and with their presentations as partial orders), phase semantics and a cut-elimination theorem. This involves, in particular, the study of the entropy relation between partial orders, and the introduction of a special class of order varieties: the series–parallel order varieties.