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