Re: Structural Rules and Exponentials
Further to Yves' message, I should like to announce that my paper is
available by anonymous ftp on theory.doc.ic.ac.uk in directory
The title and abstract are as follows:
WHAT IS A CATEGORICAL MODEL OF INTUITIONISTIC LINEAR LOGIC?
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.]