oscar@cui.unige.ch (Oscar Nierstrasz) (12/06/90)
I am looking for a good introduction to Linear Logic. I have the following seminar paper by Girard, but it is not very gentle as an introduction: %A J-Y. Girard %T Linear Logic %J Theoretical Computer Science %V 50 %I North-Holland %D 1987 %P 1-102 Can anyone provide any good pointers? Thanks in advance. Oscar Nierstrasz --------------------------------------------------------------------- Dr. O.M. Nierstrasz E-mail: oscar@cuisun.unige.ch Centre Universitaire d'Informatique Tel: 41 (22) 787.65.80 12 rue du Lac, CH-1207 Geneva Fax: 41 (22) 735.39.05 SWITZERLAND Home: 41 (22) 733.95.68 ---------------------------------------------------------------------
verwer@ruuinf.cs.ruu.nl (Nico Verwer) (12/07/90)
In article <4053@cui.unige.ch> oscar@cui.unige.ch (Oscar Nierstrasz) writes: >I am looking for a good introduction to Linear Logic. I also found the paper by Girard in TCS hard to read as an introduction. An article on LL which made me understand what it's all about was "Towards a geometry of interaction" by Jean-Yves Girard in "Categories in Computer Science and Logic", John W. Gray and Andre Scedrov, eds., Contemporary Mathematics volume 92, AMS 1989. This is in the proceedings of a conference held in 1987 in Boulder, but it appeared in print only last year. You may also want to read "Linear logic, *-autonomous categories and cofree algebras" by R.A.G. Seely, which appears in the same volume. Other references are: "Linear logic and parallelism" by J.-Y. Girard in LNCS 280 (Does anyone know if the paper in cooperation with Gianfranco Mascari, which Girard promises in the abstract has ever actually appeared?), "Linear logic and lazy computation" by J.-Y. Girard and Y. Lafont in LNCS 250, "An algebraic axiomatization of linear logic models" by Narciso Marti-Oliet and Jose Meseguer, SRI-CSL-89-11, tech. rep. SRI International. -- Nico Verwer | verwer@cs.ruu.nl Dept. of Computer Science, University of Utrecht | phone: +31 30 533921 p.o. box 80.089, 3508 TB Utrecht, The Netherlands | fax: +31 30 513791 No military intervention in the Gulf - Stop the war drive!
duchier@cs.yale.edu (Denys Duchier) (12/08/90)
In article <4053@cui.unige.ch> oscar@cui.unige.ch (Oscar Nierstrasz) writes: > I am looking for a good introduction to Linear Logic. > I have the following seminar paper by Girard, but it > is not very gentle as an introduction: > > %A J-Y. Girard > %T Linear Logic > %J Theoretical Computer Science > %V 50 > %I North-Holland > %D 1987 > %P 1-102 > > Can anyone provide any good pointers? On my desk, at this time: "What is Linear Logic?" Appendix B, in: Proofs and Types Jean-Yves Girard and Yves Lafont and Paul Taylor Cambridge Tracts in Theoretical Computer Science 7 Cambridge University Press, 1989 It also refers the reader to: Linear Logic and Lazy Computation J.Y. Girard and Y. Lafont TAPSOFT 87, vol 2, LNCS 250 Springer-Verlag Logiques, Categories et machines Y. Lafont These de doctorat University Paris VII, 1988 The Linear Abstract Machine Y. Lafont TCS (to appear) --Denys
lincoln@Neon.Stanford.EDU (Patrick D. Lincoln) (12/08/90)
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")