[LA] ================================================ AMAST Links 02 03

      What is a Categorical Model of Intuitionistic Linear Logic?
                            by G.M. Bierman

  *Abstract:* This paper re-addresses the old problem of providing a
categorical model for Intuitionistic Linear Logic (ILL). In particular
we compare the now standard model proposed by Seely to the lesser
known one proposed by Benton, Bierman, Hyland and de Paiva.
Surprisingly we find that Seely's model is unsound in that it does not
preserve equality of proofs. We shall propose how to adapt Seely's
definition so as to correct this problem and consider how this
compares with the model due to Benton et al.

  This paper is due to appear in the Proceedings of Conference on Typed
lambda calculus and Applications, LNCS, April 1995.

  An earlier version appeared as University of Cambridge Computer
Laboratory Technical Report 333, April 1994. This version is available
by anonymous ftp in directory at URL:
   ftp://theory.doc.ic.ac.uk/theory/imported/BiermanGM/