Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!lll-winken!unixhub!shelby!neon!lincoln
From: lincoln@Neon.Stanford.EDU (Patrick D. Lincoln)
Newsgroups: comp.theory
Subject: Re: Wanted: Intro to Linear Logic
Message-ID: <1990Dec7.195550.9774@Neon.Stanford.EDU>
Date: 7 Dec 90 19:55:50 GMT
References: <4053@cui.unige.ch>
Organization: Computer Science Department, Stanford University
Lines: 166

A good informal introduction to linear logic can be found in:

        @article(
EATCS,Author="Scedrov, A.",
        Title="A Brief Guide to Linear Logic",
        Journal="Bulletin of the European Assoc. for
                Theoretical Computer Science",
        Volume="41",
        Month="June",
        Year="1990",
        Pages="154-165")


If you read french, the following was written for a very wide audience:

        @article(
FrenchSciAm,Author="Girard, J.-Y.",
        Title="La Logique Lin\'eaire",
        Journal="Pour La Science, \'Edition Francaise de
        Scientific American",
        Volume="150",
        Month="April",
        Year="1990",
        pages="74-85")


A plug for some recent complexity results:
(propositional linear logic is undecidable, 
 and a natural fragment is PSPACE-complete)

	@inproceedings(
LMSS, author="Lincoln, P. and Mitchell, J.C. and Scedrov, A. and Shankar, N.",
	Title="Decision Problems for Propositional Linear Logic",
	Booktitle="Proc. 31st {IEEE} Symp. on Foundations of Computer Science",
	pages="662--671",
	Year="1990")


More references than you really wanted:

        @article(
LL,Author="Girard, J.-Y.",
        Title="Linear Logic",
        Journal="Theoretical Computer Science",
        Volume="50", 
        Year="1987",
        pages="1-102")

        @article(
Mult,Author="Girard, J.-Y.",
        Title="Multiplicatives",
        Journal="{Rendiconti del Seminario Matematico
        dell' Universit\'a e Politecnico Torino, Special Issue on
        Logic and Computer Science}",
        Year="1987",
        pages="11-33")

        @inproceedings(
Quant,Author="Girard, J.-Y.",
        Title="Quantifiers in Linear Logic",
        Booktitle="{Proc. of the SILFS Conference, Cesena, Italy}",
        Month="January",
        Year="1987")

        @misc(
GirardBoulder,Author="Girard, J.-Y.",
        Title="Towards a Geometry of Interaction",
        HowPublished="{In: Contemporary Math. 92, Amer. Math. Soc.}",
        Year="1989",
        Note="69-108")

        @inproceedings(
GeomInterI,Author="Girard, J.-Y.",
        Title="Geometry of Interaction {I}: Interpretation of System {F}",
        Booktitle="Logic Colloquium '88",
        Editors="R. Ferro et al.",
        Publisher="North-Holland",
        Address="Amsterdam",
        Year="1989")

        @misc(
GeomInterII,Author="Girard, J.-Y.",
        Title="Geometry of Interaction {II}: Deadlock-Free Algorithms",
        HowPublished="{In: Springer LNCS 417}",
        Year="1990")

        @inproceedings(
Lazy,Author="Girard, J.-Y. and Y. Lafont",
        Title="Linear Logic and Lazy Computation",
        Booktitle="{TAPSOFT '87, Volume 2}",
        Publisher="{Springer LNCS 250}",
        Year="1987",
        pages="52-66")

        @book(
ProofsTypes,Author="Girard, J.-Y. and Y. Lafont and P. Taylor",
        Title="Proofs and Types",
        Publisher="Cambrige Tracts in Theoretical Computer Science,
        Cambridge University Press",
        Year="1989")

        @inproceedings(
BLL,Author="Girard, J.-Y. and A. Scedrov and P.J. Scott",
        Title="Bounded Linear Logic: A Modular Approach to
        Polynomial Time Computability",
        Booktitle="Proc. Math. Sci. Institute Workshop on
        Feasible Mathematics, Cornell University, June, 1988",
        Editors="S.R. Buss and P.J. Scott",
        Publisher="Birkhauser",
        Year="1990")

	@phdthesis(
Bellin, Author="G. Bellin",
	title = "Mechanizing Proof Theory:
		Resource-Aware Logics and
		Proof-Transformations to Extract Implicit Information",
	school="Stanford University",
	year="1990")

        @article(
DanosRegnier89,Author="Danos, V. and L. Regnier",
        Title="The Structure of Multiplicatives",
        Journal="Archive for Mathematical Logic",
        Volume="28",
        Year="1989",
        pages="181-203")

        @inproceedings(
Cerrito90,Author="Cerrito, S.",
        Title="A Linear Semantics for Allowed Logic Programs",
        Booktitle="Proc. 5-th {IEEE} Symp. on Logic in Computer Science,
        Philadelphia",
        Month="June",
        Year="1990")

        @inproceedings(
AndreoliPareschi,Author="Andreoli, J.-M. and R. Pareschi",
        Title="Linear Objects: Logical Processes with Built-In Inheritance",
        Booktitle="Proc. 7-th International Conference on 
        Logic Programming, Jerusalem",
        Month="May",
        Year="1990")

        @inproceedings(
GunterGehlot89,Author="Gunter, C.A. and V. Gehlot",
        Title="Nets as Tensor Theories",
        Booktitle="Proc. 10-th International Conference on Application and
        Theory of Petri Nets, Bonn",
        Editor="G. De Michelis",
        Year="1989",
        pages="174-191")

        @misc(
Meseguer89,Author="Marti-Oliet, N. and J. Meseguer",
        Title="From {Petri} Nets to Linear Logic",
        HowPublished="{In: Springer LNCS 389, ed. by D.H. Pitt et al.}",
        Year="1989",
        Note="313-340")

        @article(
Avron,Author="Avron, A.",
        Title="The Semantics and Proof Theory of Linear Logic",
        Journal="Theoretical Computer Science",
        Volume="57",
        Year="1988",
        pages="161-184")