From: Gavin.Bierman@cl.cam.ac.uk
Newsgroups: fj.mail-lists.types
Subject: Term Assignment for ILL
Date: 17 Aug 92 20:52:13 GMT
Distribution: fj

To: linear@cs.stanford.edu
Date: Thu, 13 Aug 92 17:43:43 +0100

The following paper is now available by anonymous ftp.

               TERM ASSIGNMENT FOR INTUITIONISTIC LINEAR LOGIC

         Nick Benton, Gavin Bierman, Valeria de Paiva & Martin Hyland
                           University of Cambridge

We consider the problem of deriving a term assignment system for 
intuitionistic linear logic (actually only the multiplicative fragment 
for the moment). Our system differs from previous calculi (e.g. that of 
Abramsky) and has two important properties which they lack. These are the 
*substitution property* (the set of valid deductions is closed under 
substitution) and *subject reduction* (reduction on terms is well-typed). 
We have approached the derivation of a term assignment system in two ways

    1. By considering a *linear* natural deduction system. We can then 
    consider the connectives and their correct formulation. We use the 
    Curry-Howard correspondence to form a term assignment system.

    2. By taking the sequent calculus formulation, as given by Girard. 
    We have considered the rules using our categorical model (details below). 
    By considering the naturality properties of each rule, we can derive 
    a term assignment system.

We show that these two approaches provide equivalent logics and term 
assignment systems. (We give a procedure for mapping proofs from one system 
to the other). 

The main difference between our system and others is in the formulation 
of the *promotion* rule. Our sequent rule is

     x1:!A1,...,xn:!An |- e : B
    ----------------------------
     z1:!A1,...,zn:!An |- promote z1,...,zn for x1,...,xn in e : !B

(note the (vital) change of free variable names)

The natural deduction version is

    D1 |- e1:!A1 
    ...
    Dn |- en:!An         x1:!A1,...,xn:!An |- e : B
   -------------------------------------------------
    D1,...,Dn |- promote e1,...,en for x1,...,xn in e : !B
     
We then consider *reduction* in both systems. In the natural deduction 
system, we can derive beta-reductions and commuting conversions. In the 
sequent system, by considering cut-elimination, we have derived many more 
reductions. We show that all these reductions are instances of the naturality 
equations given by our categorical model. The computational significance 
of these equations is discussed.

_______________________________________________________________________________
This paper is available by anonymous ftp from IMPERIAL COLLEGE. If you can 
not use ftp, send me your postal address.

% ftp theory.doc.ic.ac.uk
Name: anonymous
Password: <<Your e-mail address>>
ftp> cd theory/papers/dePaiva
ftp> binary
ftp> get taill.dvi.Z
ftp> bye

The BibTeX entry for this paper is

@techreport{benton92,
    author = "Nick Benton and Gavin Bierman and Valeria de Paiva and Martin 
    Hyland",
    title = "Term Assignment for Intuitionistic Linear Logic",
    number = 262,
    institution = "Computer Laboratory, University of Cambridge",
    month = aug,
    year = 1992
}