###
LINEAR LOGIC, *-AUTONOMOUS CATEGORIES AND COFREE COALGEBRAS

by R.A.G. Seely

ABSTRACT:

A brief outline of the categorical characterisation of Girard's linear
logic is given, analagous to the relationship between cartesian closed
categories and typed lambda-calculus. The linear structure amounts to a
*-autonomous category: a closed symmetric monoidal category G with finite
products and a closed involution. Girard's exponential operator, ! , is a
cotriple on G which carries the canonical comonoid structure on A with
respect to cartesian product to a comonoid structure on !A with respect to
tensor product. This makes the Kleisli category for ! cartesian closed.

This paper appeared in

Contemporary Mathematics

Volume 92, 1989