[Prev][Next][Index][Thread]

Full ILL paper



The following paper is now available by anonymous ftp. 

       FULL INTUITIONISTIC LINEAR LOGIC

      Martin Hyland and Valeria de Paiva
            University of Cambridge


In this paper we give a brief treatment of a theory of proofs for a
system of Full Intuitionistic Linear Logic. Since Girard and Lafont's
original paper on Intuitionistic Linear Logic it seems to have been
generally assumed that the multiplicative disjunction, {\em par}, does
not make sense outside the context of Classical Linear Logic; in
particular par was thought to present problems for an interpretation
of proofs as functions.  However the connective par does have an
entirely natural interpretation in models which appeared in the second
author's doctoral dissertation, and it is our intention to make good
the claim that full intuitionistic is a significant dialect of linear
logic.

The novelty of Full Intuitionistic Linear Logic lies in its treatment
of the interaction between par (which has the same 2-sided
sequent-calculus rules as the Classical Linear Logic par) and the
linear implication (which only satisfies the intuitionistic properties
of an implication).  We take as the main initial problem to be
overcome the observation of Schellinx that cut elimination fails
outright for the intuitive formulation of such a logical system.  Our
response is to develop a term assignment system which gives an
interpretation of proofs as some kind of non-deterministic function
(which appears as a sequence of partial functions evaluated in
parallel). In this way we find a system which {\em does} enjoy cut
elimination. The system is a direct result of an analysis of the
categorical semantics, though we make an effort to present the system
as if it were purely a proof-theoretic construction.


-----------
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
To: 
Name: anonymous
Password: <<Your e-mail address>>
ftp> cd theory/papers/dePaiva
ftp> binary
ftp> get fill.dvi.Z
ftp> bye


The BibTeX entry for this paper is

@unpublished{depaiva93,
    author = "Valeria de Paiva and Martin  Hyland",
    title = "Full Intuitionistic Linear Logic (Extended Abstract)",
    institution = "Computer Laboratory, University of Cambridge",
    month = May,
    year = 1993,
    note = ``To appear in Annals of Pure and Applied Logic''
}

Valeria de Paiva

------------------------------------------------------------------------------
Valeria de Paiva,                  |
University of Cambridge            | Phone: +44 (0)223 334418
Computer Laboratory                | Fax: +44 (0)223 334678
New Museums Site, Pembroke Street  | JANET: Valeria.Paiva@uk.ac.cam.cl
Cambridge CB2 3QG, England, UK     | Internet: Valeria.Paiva@cl.cam.ac.uk
------------------------------------------------------------------------------