Xref: utzoo sci.math:17498 sci.logic:1282 comp.theory:2001
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!unix.cis.pitt.edu!dsinc!ub!uhura.cc.rochester.edu!rochester!rocksanne!mum.wrc.xerox.com!mantha
From: mantha@mum.wrc.xerox.com (S. Mantha (co-op))
Newsgroups: sci.math,sci.logic,comp.theory
Subject: Re: Linear Logic
Keywords: Linear Logic
Message-ID: <815@rocksanne.WRC.XEROX.COM>
Date: 17 May 91 14:53:50 GMT
References: <3023@puck.sw.mcc.com> <1991May16.232218.8032@newshost.anu.edu.au> <1991May17.082838.3274@forwiss.uni-passau.de>
Sender: news@WRC.XEROX.COM
Reply-To: mantha.wbst128@xerox.com
Lines: 49

In article <1991May17.082838.3274@forwiss.uni-passau.de>,
mueck@hal.fmi.uni-passau.de (Andreas Mueck) writes:
|>In article <1991May16.232218.8032@newshost.anu.edu.au>
gar@earth.anu.edu.au (Greg Restall) writes:
|>>In article <3023@puck.sw.mcc.com> meredith@puck.sw.mcc.com (LG
Meredith) writes:
|>>* Are there any widely respected introductions to Linear Logic? I'm
|>>* simply too stupid to follow Girard's positively Joycean expositions on
|>>* the subject. I am, however, interested in its applications to semantics
|>>* for OOLs.
|>>
|>There is a good paper of Samson Abramsky named "Computational Interpretation
|>of Linear Logic" (Imperial College Research Report DOC 90/20). It
gives a good
|>intro to Intuitionistic LL as well as to Classical LL.
|>
|>Andy Mueck, University of Passau, P.O. Box 2540, D-8390 Passau, FRG
|>mueck@unipas.fmi.uni-passau.de
|>
|>   ..... god save the Rolling Stones
               
There is another paper by Yves Lafont called "Introduction to Linear Logic".
It  is from  "Lecture notes for the Summer School on Constructive Logics and 
Category Theory (Isle of Thorns, August 1988). This is a readable paper too.
It introduces linear logic from the denotational point of view (coherence
spaces .... ) and also talks about sequent calculus and proof nets. 

After trying to read Girard's original paper, "Finnegan's Wake" reads like
"TV Digest".

A (probably very stupid) question: The unary connective "!" is supposed to be
the modality "ofcourse". In what sense is it "of course"? Girard mentions
that "!" and "?" are like the modal operators "box" and "diamond". Is it 
possible to give a "possible worlds" semantics for formulae with "!" and
"?".  Girard talks about being able to use something only once or 
as many times as needed and says that this is related to the philosophical
tradition of "strict implication" which originates from Lewis. Could
someone explain this?

The traditional separation of syntax from semantics (starting from Hilbert)
and the identification of "meaning" with "truth" is probably somewhat
restrictive, specially if logic is to be used to specify computations.
But these new logics (at least at this point in time and certainly to me)
seem to lack the simplicity of the traditional logical apparatus. 

I am only too willing to be proved wrong and to be educated on this. 

cheers
Surya