Re: Structural Rules and Exponentials

• To: linear@cs.stanford.edu
• Subject: Re: Structural Rules and Exponentials
• From: G M Bierman <Gavin.Bierman@cl.cam.ac.uk>
• Date: Fri, 10 Feb 1995 17:29:40 +0000
• Approved: types@dcs.gla.ac.uk

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
/theory/imported/BiermanGM. 

The title and abstract are as follows:

     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.]

• Prev: Higher-Order Logic Programming
• Next: For you perhaps
• Index(es):
  • Main
  • Thread