Return-Path: <@Sunburn.Stanford.EDU:sa@doc.ic.ac.uk> Date: Thu, 10 Dec 1992 16:03:13 +0000 (GMT) From: Samson Abramsky Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII To: linear@cs.stanford.edu Subject: New Foundations for the Geometry of Interaction (full version) Sender: lincoln@cs.stanford.edu --text follows this line-- The full version of ``New Foundations for the Geometry of Interaction'' by myself and Radha Jagadeesan is now available by anonymous-ftp from theory.doc.ic.ac.uk in compressed form as papers/Abramsky/nfgi.{dvi,ps}.Z. (An extended abstract was published in the Proceedings of LICS `92). Samson Abramsky Return-Path: <@Sunburn.Stanford.EDU:log.mian.su!bekl@kremvax.hq.demos.su> To: linear@cs.stanford.edu Organization: Steklov Mathematical Institute, Moscow From: bekl@log.mian.su (Lev D. Beklemishev) Date: Tue, 5 Jan 93 15:48:48 +0300 (MSK) Subject: Constant-Only LL is undecidable Sender: lincoln@cs.stanford.edu --text follows this line-- We prove that propositional Linear Logic containing either only one literal or only one constant \bottom is of the extreme expressive power. As a corollary, both one-literal Linear Logic and constant-only Linear Logic turned out to be undecidable. P.Lincoln, J.Mitchell, A.Scedrov, and N.Shankar (1990) proved the undecidability of full propositional Linear Logic (containing Multiplicatives, Additives, and Exponentials). We proved the undecidability for a restricted fragment of Linear Logic (the so-called generalized Horn fragment) containing only four literals (LICS'92). Here we prove that any standard Minsky machines can be directly encoded in each of the two following fragments of Linear Logic: 1. A one-literal fragment of LL. It consists of sequents of the form Gamma, !Delta |- p where multisets Gamma and Delta contain (a) the only positive literal p, (b) no other literals, (c) neither negative literals, nor constants, nor negations, (d) two multiplicatives: tensor product and linear implication, (e) one additive: & (or +), (f) no exponentials (! appears only outside of formulas from the multiset !Delta). 2. A constant-only fragment of LL. It consists of sequents of the form Gamma, !Delta |- \bottom where multisets Gamma and Delta contain (a) no literals at all, (b) the only constant \bottom, (c) neither other constants, nor negations, (d) only one multiplicative: linear implication, (e) one additive: & (or +), (f) no exponentials (! appears only outside of formulas from the multiset !Delta). Our encoding of computations of standard counter machines by derivations of the corresponding sequents is based on a complete computational characterization of certain fragments of Linear Logic. Best regards, Max Kanovich. Return-Path: <@Sunburn.Stanford.EDU:perun!ips.ac.msk.su!mian!log!bekl%log.mian.su@uu.psi.com> To: linear@cs.stanford.edu Organization: Steklov Mathematical Institute, Moscow From: bekl@log.mian.su (Lev D. Beklemishev) Date: Sun, 10 Jan 93 17:13:13 +0300 (MSK) Subject: Complexity of Constant-Only Fragments of LL Sender: lincoln@cs.stanford.edu --text follows this line-- For ordinary logics (e.g. for classical or intuitionistic ones), their one-literal and, especially, constant-only fragments are essentially simpler than the corresponding full logics (with unrestricted number of literals.) The point is that the simulating of PSPACE-complete problems, a priori, requires unrestricted number of variables. For example, the proof of PSPACE-completeness of the implicative fragment of intuitionistic logic as well as of quantified Boolean formulas essentially uses unrestricted number of variables. Contrary to what might be expected, we prove that one-literal and even constant-only fragments of Linear Logic are of the same expressive power as the corresponding full parts of LL with infinite number of literals. In abbreviations like MLL, MALL, MELL, MAELL LL indicates Propositional Linear Logic, M indicates Multiplicatives: Tensor Product and Linear Implication, A indicates Additives: & and \oplus, E indicates the storage operator !. Let us recall that 1. MLL is NP-complete (Kanovich, 1991). 2. MALL is PSPACE-complete (Lincoln, Mitchell, Scedrov, and Shankar, 1990) 3. MELL can encode Petri Nets reachability. 4. MAELL is undecidable (Lincoln, Mitchell, Scedrov, and Shankar, 1990) We consider One-literal parts of these fragments which contain (a) the only one positive literal p, (b) no other literals, (c) neither negative literals, nor constants, nor negations, (d) in the case E, the exponential ! is allowed to appear only outside of formulas. We proved the following results: 1. One-literal MLL is NP-complete (Kanovich, 1992). 2. One-literal MALL is PSPACE-complete (Kanovich, this message). 3. One-literal MELL can encode Petri Nets reachability. (Kanovich, this message). 4. One-literal MAELL can directly simulate standard Minsky machines, and, hence, it is undecidable (Kanovich, 1992, December). We consider Constant-only parts of the fragments of LL in question which contain (a) no literals at all, (b) the only constant \bottom, (c) neither other constants, nor negations, (d) only one multiplicative: linear implication, (e) in the case E, the exponential ! is allowed to appear only outside of formulas. The following results are proved: 1. Constant-only MLL is NP-complete (Lincoln and Winkler, 1992). 2. Constant-only MALL is PSPACE-complete (Kanovich, this message). 3. Constant-only MELL can encode Petri Nets reachability. (Kanovich, this message). 4. Constant-only MAELL can directly simulate standard Minsky machines, and, hence, it is undecidable (Kanovich, 1992, December). In order to establish PSPACE-hardness, we prove that the purely implicative fragment of intuitionistic logic can be directly simulated in One-literal MALL, as well as in Constant-only MALL. My best regards, Max Kanovich. Return-Path: <@Sunburn.Stanford.EDU:rags@triples.math.mcgill.ca> Date: Tue, 19 Jan 93 14:26:43 EST From: rags@triples.Math.McGill.CA (Robert A. G. Seely) To: linear@cs.stanford.edu Subject: Coherence for weakly distributive categories Sender: lincoln@cs.stanford.edu --text follows this line-- We wish to announce that the following paper may be obtained by anonymous ftp (details below) or directly from the authors. Natural deduction and coherence for weakly distributive categories by R.F. Blute, J.R.B. Cockett, R.A.G. Seely, T.H. Trimble (The abstract follows, but first let us highlight some points for two specific audiences:) Some points that might interest categorists: * Proof of coherence for weakly distributive categories. (These are a natural generalization of monoidal categories to include a second "interwoven" tensor, the interweaving given by tensorial strength - the "weak distributivities".) * New uses of logical techniques to prove coherence: proof nets and empires (from linear logic). * Conservativity of the extension to *-autonomous categories. (Here we mean that the unit of the adjunction is fully faithful.) Some points that might interest linear logicians: * By studying the weak fragment of linear logic that weakly distributive categories represent, one can better get to the structure of PAR vis a vis TIMES (without duality confusing the issue). * Units are handled in a constructive version of the usual treatment: we introduce "thinning links" to attach units to the net structure so as to preserve the "acyclic and connected" net criterion, and then determine how these links can be moved about without disturbing the essential structure (coherence). * Coherence represents (part of) the structure of the proof theory of logic, namely when do proof structures represent "the same proof". ========================================================================== ABSTRACT We define a two sided notion of proof nets, suitable for categories, like weakly distributive categories, which have the two-tensor structure (TIMES/PAR) of linear logic, but lack a NEGATION operator. These proof nets have a structure more closely parallel to that of traditional natural deduction than Girard's one-sided nets do. In particular, there is no cut, and cut elimination is replaced by normalization. We prove a sequentialization theorem for these nets and the corresponding sequent calculus, and deduce the coherence theorem for weakly distributive categories. We also extend these techniques to cover the case of non-symmetric ("planar") tensors. We further extend the treatment of coherence to include the units for the tensors, giving a characterization of the Lambek equivalence relation on deductions (i.e. equality of morphisms) in terms of the notion of empire. Finally, we derive a conservative extension result for the passage from weakly distributive categories to *-autonomous categories. ========================================================================== To obtain a copy by anonymous ftp, ftp triples.math.mcgill.ca and login as anonymous - use your email address as password; cd to the directory pub/rags/nets and take the appropriate file: either nets.dvi.Z or nets.ps.Z (you will have to uncompress them at your own site). Contact rags@math.mcgill.ca if you have any trouble with the ftp process or with printing the files at your site. Return-Path: <@Sunburn.Stanford.EDU:voronkov@cliquot.loria.fr> Date: Sat, 23 Jan 93 23:06:57 +0100 From: Voronkov Andrei To: linear@cs.stanford.edu Subject: LPAR93 deadline extension and CFP Sender: lincoln@cs.stanford.edu --text follows this line-- LPAR'93 - 4th International Conference on Logic Programming and Automated Reasoning Call for Papers St.Petersburg, Ship "Michail Lomonosov" July 13-20, 1993 LPAR'93 is an international conference traditionally held in Russia since 1990. It aims at bringing together researchers interested in logic programming and automated reasoning. LPAR'93 is also an excellent opportunity to become better acquainted with research in Russia and other countries of the former Soviet Union. INVITED SPEAKERS: Alan Bundy (Edinburgh University, UK) (Title to be announced) Herve Gallaire (Xerox, France) Research in Logic Programming and Deductive Databases: The Impact on Industry Ryuzo Hasegawa (ICOT, Japan) Model Generation Theorem Provers on PIM Peter Wegner (Brown University, USA) Reasoning Versus Modeling in Computer Science Nail Zamov (Kazan University, Russia) Theorem proving in Kazan' TUTORIALS: Jean-Marc Andreoli, Remo Paresci (ECRC) Linear Logic Programming Evan Tick (University of Oregon) An Advanced Tutorial in Concurrent Logic Programming: Paradigms and Implementation Leo Bachmair (SUNY at Stony Brook), Harald Ganzinger(Max Plank Institut f\"ur Informatik) Paramodulation-based Theorem Proving for First-Order Logic with Equality PROGRAM COMMITTEE: Dmitri Boulanger (Belgium/Russia) Mats Carlsson (Sweden) Philippe Codognet (France) Danny De Schreye (Belgium) Norbert Eisinger (Germany) Harald Ganzinger (Germany) Ryuzo Hasegawa (Japan) Steffen Hoelldobler (Germany) Deepak Kapur (USA) Jean-Louis Lassez (USA) Alexander Leitsch (Austria) Giorgio Levi (Italy) John Lloyd (UK) Ewing Lusk (USA) Dale Miller (USA) Jack Minker (USA) Gregory Mints (USA/Estonia) Alan Mycroft (UK) Lee Naish (Australia) Hans-Jurgen Ohlbach (Germany) Michel Parigot (France) Frank Pfenning (USA) Vladimir Sazonov (Russia) Marek Sergot (UK) Mark Stickel (USA) Pascal Van Hentenryck (USA) Konstantin Vershinin (Ukraine) Andrei Voronkov (Russia) - chair Nail Zamov (Russia) ORGANIZING COMMITTEE: Eugene Dantsin (Russia) Robert Freidson (Russia/USA) - chair Andrei Voronkov (Russia) TOPICS OF INTEREST include, but are not restricted to: Constraints Deductive databases Formal methods in software and hardware Implementation techniques Inductive theorem proving Logical Frameworks LPAR in artificial intelligence Meta-programming Parallelism and concurrency Program synthesis and verification Programming in constructive logic Theorem proving Theory and foundations Unification theory and rewriting Authors are invited to submit 5 copies of their manuscripts to the address: Andrei Voronkov - LPAR'93 CRIN-CNRS & INRIA Lorraine Batiment Loria, BP 239 54506 Vandoeuvre-les-Nancy Cedex France For countries where copying may be a problem one copy will be sufficient. Email TeX/LaTeX submissions are acceptable from the countries with postal problems. Proceedings will be published in the series "Lecture Notes in Artificial Intelligence" by Springer Verlag. (Proceedings of the previous conferences were published in LNAI vv.592 and 624). There are three kinds of submissions: long papers (up to 12 pages), short papers (up to 6 pages), or system descriptions (up to 3 pages). All papers must be written in English. Submissions should be accompanied by a one-page abstract sent either to the same address or (preferably) by email to voronkov@loria.fr. The abstract should include author's name(s), affiliation, postal and email addresses. The program will also include a special session on system demonstrations (IBM PCs and SPARCstations) and several tutorials delivered by major researchers in the field. IMPORTANT DATES: Submission: February 1 Notification: March 20 Final Version: April 20 Further information may be obtained at the email address voronkov@loria.fr. ======================================================= \documentstyle[11pt]{article} \topmargin -1.5cm \oddsidemargin +0.1cm \textheight 25.5cm \textwidth 16.5cm \setlength{\parindent}{0cm} \setlength{\parskip}{1.8ex} \begin{document} \framebox[1.2cm][c]{\hspace{1.6mm}\Huge "\hspace{-1mm}("}\hspace{.5cm} \begin{minipage}[c]{14.4cm} \begin{center} {\Large\bf LPAR'93 -- 4th International Conference on\vspace{2mm}\\ Logic Programming and Automated Reasoning} \end{center} \end{minipage} \begin{center} {Call for Papers}\\ \ \\ {\large St.Petersburg, Ship ``Michail Lomonosov'' \\ July 13-20, 1993} \end{center} LPAR'93 is an international conference traditionally held in Russia since 1990. It aims at bringing together researchers interested in logic programming and automated reasoning. LPAR'93 is also an excellent opportunity to become better acquainted with research in Russia and other countries of the former Soviet Union. {\bf Invited speakers:} \begin{tabbing} Q\=QQ\=\kill \> Alan Bundy (Edinburgh University, UK)\\ \> \> \em (Title to be announced)\\ \> Herve Gallaire (Xerox, France)\\ \> \> \em Research in Logic Programming and Deductive Databases: The Impact on Industry\\ \> Ryuzo Hasegawa (ICOT, Japan)\\ \> \> \em Model Generation Theorem Provers on PIM\\ \> Peter Wegner (Brown University, USA)\\ \> \> \em Reasoning Versus Modeling in Computer Science\\ \> Nail Zamov (Kazan University, Russia)\\ \> \> \em Theorem proving in Kazan' \end{tabbing} {\bf Tutorials:} \begin{tabbing} Q\=QQ\=\kill \> Jean-Marc Andreoli, Remo Paresci (ECRC): \\ \> \> \em Linear Logic Programming \\ \> Evan Tick (University of Oregon): \\ \> \> \em An Advanced Tutorial in Concurrent Logic Programming: Paradigms and Implementation\\ \> Leo Bachmair (SUNY at Stony Brook), Harald Ganzinger(Max Plank Institut f\"ur Informatik)\\ \> \> \em Paramodulation-based Theorem Proving for First-Order Logic with Equality \end{tabbing} {\bf Program Committee:} \begin{tabbing} Q\= Dmitri Boulanger (Belgium/Russia)MMM \= \kill \> Dmitri Boulanger (Belgium/Russia) \> Mats Carlsson (Sweden)\\ \> Philippe Codognet (France) \> Danny De Schreye (Belgium)\\ \> Norbert Eisinger (Germany) \> Harald Ganzinger (Germany)\\ \> Ryuzo Hasegawa (Japan) \> Steffen H{\"o}lldobler (Germany)\\ \> Deepak Kapur (USA) \> Jean-Louis Lassez (USA) \\ \> Alexander Leitsch (Austria) \> Giorgio Levi (Italy)\\ \> John Lloyd (UK) \> Ewing Lusk (USA)\\ \> Dale Miller (USA) \> Jack Minker (USA)\\ \> Gregory Mints (USA/Estonia) \> Alan Mycroft (UK)\\ \> Lee Naish (Australia) \> Hans-Jurgen Ohlbach (Germany)\\ \> Michel Parigot (France) \> Frank Pfenning (USA)\\ \> Vladimir Sazonov (Russia) \> Marek Sergot (UK)\\ \> Mark Stickel (USA) \> Pascal Van Hentenryck (USA)\\ \> Konstantin Vershinin (Ukraine) \> Andrei Voronkov (Russia) - chair\\ \> Nail Zamov (Russia) \end{tabbing} \newpage {\bf Organizing Committee:} \begin{tabbing} Q\=\kill \> Eugene Dantsin (Russia) \\ \> Robert Freidson (Russia/USA) - chair\\ \> Andrei Voronkov (Russia) \end{tabbing} {\bf Topics of interest} include, but are not restricted to: \begin{tabbing} Q\=Formal methods in software and hardwareQQ\=\+\kill Constraints \> Deductive databases \\ Formal methods in software and hardware \> Implementation techniques \\ Inductive theorem proving \> Logical Frameworks \\ LPAR in artificial intelligence \> Meta-programming \\ Parallelism and concurrency \> Program synthesis and verification \\ Programming in constructive logic \> Theorem proving \\ Theory and foundations \> Unification theory and rewriting \end{tabbing} Authors are invited to submit 5 copies of their manuscripts to the address: \begin{center} Andrei Voronkov -- LPAR'93\\ CRIN-CNRS \& INRIA Lorraine\\ Batiment Loria, BP 239 \\ 54506 Vandoeuvre-les-Nancy Cedex\\ France \end{center} For countries where copying may be a problem one copy will be sufficient. Email \TeX/\LaTeX\ submissions are acceptable from the countries with postal problems. Proceedings will be published in the series ``Lecture Notes in Artificial Intelligence'' by Springer Verlag. (Proceedings of the previous conferences were published in LNAI vv.592 and 624). There are three kinds of submissions: {\em long papers\/} (up to 12 pages), {\em short papers\/} (up to 6 pages), or {\em system descriptions\/} (up to 3 pages). All papers must be written in English. Submissions should be accompanied by a one-page abstract sent either to the same address or (preferably) by email to voronkov@loria.fr. The abstract should include author's name(s), affiliation, postal and email addresses. The program will also include a special session on system demonstrations (IBM PCs and SPARCstations) and several tutorials delivered by major researchers in the field. {\bf Important dates:} \begin{tabbing} Q\=Final Version:\ \=\+\kill Submission: \> February 1\\ Notification: \> March 20\\ Final Version: \> April 20 \end{tabbing} Further information may be obtained at the email address voronkov@loria.fr. \end{document} Return-Path: <@Sunburn.Stanford.EDU:danos@logique.jussieu.fr> Date: Mon, 25 Jan 93 13:48:28 +0100 From: danos@logique.jussieu.fr To: Linear@cs.stanford.edu Subject: Summer School in ``Logic in Computer Science'' Sender: lincoln@cs.stanford.edu --text follows this line-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Summer School announcement and latex file of the corresponding poster +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ First International Summer School in Logic for Computer Science "PROOF THEORY and FOUNDATIONS OF PROGRAMMING" June 28 -- July 9, 1993, University of Chambery (France) Parc Scientifique Savoie-Technolac, Le Bourget-du-lac The series of International Summer Schools in Logic for Computer Science is part of the "Euroconferences" program of the European Community, and is supported by the European Association for Computer Science Logic. It is intended primarily for young researchers in Computer Science or in Mathematics, who are interested in "Logical Tools and Methods for Computer Science", from the viewpoints of both theory and applications. Each school is devoted to a specific topic, whose theoretical foundations have developed recently, and which has promising applications. The topic of this year's school is "Proof Theory and Foundations of Programming". The lectures will analyse the relations between formal proofs and programs, from their historical roots in Proof Theory and Lambda Calculus to their most recent theoretical and practical advances. The well-known correspondence between constructive proofs and functional programs provides a theoretical framework for the mathematization of programming, and has important consequences, which include program correctness, modularity, and reusability. The subject is undergoing at present impressive developments in various directions, including automatic extraction of programs from proofs, correspondence between classical logic and imperative program constructs, control of computational complexity at the level of proof systems, and new computational paradigms derived from proof theory. During the two week school participants would be able to attend comprehensive courses as well as informal talks, and to take active part in discussions of open problems. The following courses will be offered. J.Y. GIRARD (Marseille, France): Fundamentals of Proof Theory: Proofs and Types. S. RONCHI (Torino, Italy): Fundamentals of Lambda-calculus S. BERARDI (Torino, Italy): Program Extraction from Constructive Proofs J.L. KRIVINE (Paris, France): Programming with Proofs in Second Order Logic D. LEIVANT (Bloomington, USA): Computational Complexity inherent in Type Systems M. PARIGOT (Paris, France): Algorithmic Interpretations of Classical Logic L. REGNIER (Marseille, France): New Models of Execution derived from Proof Nets A. SCEDROV (Philadelphia, USA): Linear Logic J. TIURYN (Warsaw, Poland): Type Reconstruction The school will take place at the University of Chambery, near Lake Bourget (``Lac du Bourget'') in the High Alps. In addition to its stunning alpine setting, Chambery offers a broad range of activities and recreations, benefitting from its proximity to both high mountains and an 18 km long lake. Participants will also be offered organized activities. The participation fees amount to 5200 FF, which include registration fees and living expenses (lodging, meals, coffee breaks, ...etc). A limited number of grants will be offered. Deadline for Applications: April 15th 1993 For further information and application forms for participation and for grants please contact: M. Parigot / School LCS, Laboratoire de Logique, UFR de Math\'ematiques, Universit\'e Paris 7, 2 place Jussieu, 75251 Paris Cedex 05, France e-mail: school@logique.jussieu.fr School Director: M. Parigot Organizing Committee: R. David, N. Bernard, J. Doyen +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Here is the latex file of a poster of the School "PROOF THEORY and FOUNDATIONS OF PROGRAMMING", that can be printed and stuck. A big and colour poster is a also available on request at school@logique.jussieu.fr +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ \documentstyle{report} \textwidth 17.8cm \textheight 26cm \topmargin -2cm \oddsidemargin -1cm \evensidemargin -1cm \pagestyle{empty} \begin{document} \begin{center} {\Large {\bf First International Summer School in Logic for Computer Science}} \end{center} \vspace{3 mm} \begin{center} {\Huge { PROOF THEORY}}\\ \vspace{2 mm} \hspace{-5 mm}{\Large {\bf \&}}\\ \vspace{3.5 mm} {\Huge { FOUNDATIONS OF PROGRAMMING}} \end{center} \vspace{3 mm} \begin{center} {\Large June 28 -- July 9, 1993, University of Chamb\'ery (France)}\\ \vspace{1.5 mm} {\large Parc Scientifique Savoie-Technolac, Le Bourget-du-lac} \end{center} \vspace{7 mm} \noindent The series of International Summer Schools in Logic for Computer Science is part of the {\it Euroconferences} program of the European Community, and is supported by the European Association for Computer Science Logic. It is intended primarily for young researchers in Computer Science or in Mathematics, who are interested in {\it Logical Tools and Methods for Computer Science}, from the viewpoints of both theory and applications. Each school is devoted to a specific topic, whose theoretical foundations have developed recently, and which has promising applications. \medskip \ \noindent \begin{minipage}[t]{8.4cm} \begin{center} { {\bf J.Y. GIRARD}, { Marseille, France}\\ {\it Fundamentals of Proof Theory: Proofs and Types}}\\ \medskip { {\bf S. RONCHI}, { Torino, Italy} \\ {\it Fundamentals of $\lambda$-calculus}}\\ \medskip { {\bf S. BERARDI}, { Torino, Italy} \\ {\it Program Extraction from Constructive Proofs}}\\ \medskip { {\bf J.L. KRIVINE}, { Paris, France} \\ {\it Programming with Proofs in Second Order Logic}}\\ \medskip { {\bf D. LEIVANT}, { Bloomington, USA} \\ {\it Computational Complexity inherent in Type Systems}}\\ \medskip { {\bf M. PARIGOT}, { Paris, France}\\ {\it Algorithmic Interpretations of Classical Logic}} \\ \medskip { {\bf L. REGNIER}, { Marseille, France}\\ {\it New Models of Execution derived from Proof Nets}} \\ \medskip { {\bf A. SCEDROV}, { Philadelphia, USA}\\ {\it Linear Logic}}\\ \medskip { {\bf J. TIURYN}, { Warsaw, Poland}\\ {\it Type Reconstruction}}\\ \end{center} \end{minipage}\ \hspace{1.3cm} \begin{minipage}[t]{7.9cm} The topic of this year's school is {\it Proof Theory and Foundations of Programming}. The lectures will analyse the relations between formal proofs and programs, from their historical roots in Proof Theory and Lambda Calculus to their most recent theoretical and practical advances. The well-known correspondence between constructive proofs and functional programs provides a theoretical framework for the mathematization of programming, and has important consequences, which include program correctness, modularity, and reusability. The subject is undergoing at present impressive developments in various directions, including automatic extraction of programs from proofs, correspondence between classical logic and imperative program constructs, control of computational complexity at the level of proof systems, and new computational paradigms derived from proof theory. During the two week school participants would be able to attend comprehensive courses, whose list is indicated, as well as informal talks, and to take active part in discussions of open problems. \end{minipage} \bigskip \ \noindent The school will take place at the University of Chamb\'ery, near Lake Bourget (``Lac du Bourget'') in the High Alps. In addition to its stunning alpine setting, Chamb\'ery offers a broad range of activities and recreations, benefitting from its proximity to both high mountains and an 18 km long lake. Participants will also be offered organized activities. \noindent A limited number of {\it grants} will be offered, covering living expenses and registration fees. \medskip \begin{center} \noindent {\bf Deadline for Applications: April 15th 1993} \medskip \noindent For further information and application forms for participation and for grants please contact: \\ M. Parigot / School LCS, Laboratoire de Logique, UFR de Math\'ematiques, \\ Universit\'e Paris 7, 2 place Jussieu, 75251 Paris Cedex 05, France \\ e-mail: {\tt school@logique.jussieu.fr} \end{center} \bigskip \noindent {\large {\bf School Director}: M. Parigot \hfill\ {\bf Organizing Committee}: R. David, N. Bernard, J. Doyen} \end{document} Return-Path: <@Sunburn.Stanford.EDU,@s.ms.uky.edu,@ms.uky.edu:radek@ms.uky.edu> To: linear@cs.stanford.edu Subject: referencies inquiry Date: Tue, 16 Feb 93 01:38:49 EST From: radek@ms.uky.edu Sender: lincoln@cs.stanford.edu --text follows this line-- Would anybody send me referencies to any work dealing with possible use of linear logic in database theory? Thank you very much. Radek Vingralek ------------------------------------------------------------------------------ Radek VINGRALEK radek@ms.uky.edu radek@UKMA.bitnet radek@cs.uky.edu Office: University of Kentucky Home: 700 Woodland Ave., Apt. F 109 Dept. of Comp. Sci. Lexington, KY 40508-3423 915 Patterson Office Tower USA Lexington, KY 40506-0027 USA tel: (606) 257-6750 fax: (606) 258-1971 ----------------------------------------------------------------------------- Return-Path: <@Sunburn.Stanford.EDU:ehrhard@dmi.ens.fr> From: Thomas Ehrhard Subject: Hypercoherences To: linear@cs.stanford.edu Date: Fri, 19 Feb 93 12:22:07 WET X-Mailer: ELM [version 2.3 PL11] Sender: lincoln@cs.stanford.edu --text follows this line-- Hypercoherences: an extensional model of linear logic based on sequentiality. ----------------------------------------------------------------------------- In a previous work with Bucciarelli (see the LICS91 proceedings), we have proposed the notion of strongly stable functions on qualitative domains (or dI domains) equipped with a "coherence". We were able to build a cartesian closed category with these structures and morphisms. The basic observation was the following: 1) it is reasonable to define a notion of Kahn-Plotkin sequential functions between coherence spaces (for instance) taking the orthogonal of a coherence space E as set of "cells" on E. If x is in E and q is in orth(E), then x "fills" q if x intersects q. 2) let us call "linearly coherent" a subset A of E which is non-empty, finite, and such that: for any q in orth(E), if all the elements of A intersect q, then the intersection of A intersects q. In other words: A={x1,...,xn} is linearly coherent if, for all a1 in x1,...,an in xn, if {a1,...,an} in orth(E), then a1=...=an. In other words: any section of A which is in orth(E) is constant. Let us note CL(E) the set of all linearly coherent subsets of E. 3) then a continuous function f:E->F is sequential iff, for all A in CL(E), the set f(A) is in CL(F) and f(inter A)=inter f(A). Then we built a CCC considering couples (Q,C(Q)) where Q is a qualitative domain and C(Q) is a set of non-empty and finite subsets of Q satisfying some requirements. In this category, a morphism (Q,C(Q))->(R,C(R)) is a continuous function f:Q->R such that, for all A in C(Q), f(A) in C(R) and f(inter A)=inter f(A). (Where inter A is the intersection of A.) Such a function is called "strongly stable". This short note presents a framework were all the constructions presented in our LICS paper make sense, but where the objects admit a simpler description and where the morphisms admit a simple trace characterization. Furthermore, this framework allows to construct a model of linear logic. This model is presented in a paper which will appear soon in "Mathematical Structures in Computer Science". The objects are called "hypercoherences" (following an observation of Danos: they are hypergraphs). A hypercoherence is a pair X=(|X|,G(X)) (read G(X) as "Gamma of X") where * |X| is an enumerable set (the web) * G(X) is a set of finite and non-empty subsets of |X| The only requirement is that, for any a in |X|, {a} is in G(X). Let us note G*(X) the set of all elements of G(X) which are not singletons. G(X) is called the "coherence of X" or the "atomic coherence of X". G*(X) is called the "strict (atomic) coherence of X". Beware: G(X) is not required to be down-closed under inclusion. That is, we may have u in G(X), v non-empty subset of u but v not in G(X). Out of a hypercoherence X, one defines: * a qualitative domain qD(X). The elements of qD(X) are the subsets x of |X| such that any finite and non empty subset of x be in G(X) * a "state coherence" on qD(X), that we note C(X). An element of C(X) is a finite and non-empty subset A of qD(X) such that any finite "multisection" of A be in G(X). A multisection of A is a subset u of |X| such that any element of u be an element of an element of A, and any element of A contain an element of u. That is: u is contained in the union of A and intersects each element of A. It is easy to check that qD(X) is a qD whose web is |X|. It is also clear that any finite, non-empty and bounded subset of qD(X) is in C(X). However, there are in general elements of C(X) which are not bounded (observe for instance that any finite subset of qD(X) which contains the empty set is in C(X)) If X and Y are hypercoherences, a strongly stable map from X to Y is a continuous function qD(X)->qD(Y) such that, for all A in C(X), f(A) be in C(Y) and f(inter A)=inter f(A). Clearly, a strongly stable map is a stable map qD(X)->qD(Y), but the converse is false in general. A strongly stable map f is "linear" if it is linear as a stable map, that is f(emptyset)=emptyset and f(x union y)=f(x) union f(y). Since strongly stable functions from X to Y are stable, they admit a trace representation "a la Girard". These traces turn out to form a qD which is of the shape qD(Z) where Z is a hypercoherence definable in terms of X and Y. We describe this construction for linear strongly stable functions: Let X and Y be hypercoherences. Define a hypercoherence X-oY by: * |X-oY|=|X|x|Y| * a subset w of this web is in G(X-oY) iff it is finite, non-empty and satisfies: w1 in G(X) => w2 in G(Y) w1 in G*(X) => w2 in G*(Y) in other words: w1 in G(X) => (w2 in G(Y) and (#w2=1 => #w1=1)) (w1 and w2 are the projections of w on |X| and |Y| respectively). Then qD(X-oY) is exactly the set of all traces of linear strongly stable functions X->Y. G(X-oY) contains additionnal informations which are not used in qD(X-oY) but which are essential for defining the state coherence C(X-oY). Observe that this definition of X-oY is very similar to Girard's definition of E-oF in the framework of coherence spaces. The only diference is that here the size of the "coherence" is unbound. Tensor product of X and Y: |X tens Y|=|X|x|Y| w in G(X tens Y) iff w1 in G(X) and w2 in G(Y). This product admits a neutral element 1 (the hypercoherence whose web has only one element). It is commutative and associative. Furthermore, up to a canonical isomorphism: (X tens Y)-oZ=X-o(Y-oZ) so that we have built a monoidal closed category. Orthogonal of X: we note it Orth X. It is defined by |Orth X|=|X| u in G(Orth X) iff u is a finite and non-empty subset of |X| which is not in G*(X). Then all the usual isomorphisms are satisfied (Orth Orth X=X, contraposition, Orth X=X-oBot where Bot=Orth 1 which turns out to be isomorphic to 1, like in coherence spaces,...) The "par" is defined by duality. Cartesian product ("with"): |XxY|=|X|+|Y| (disjoint union) w is in G(XxY) iff w is a finite and non-empty subset of |X|+|Y| and w1 empty => w2 in G(Y) w2 empty => w1 in G(X) (where w1 is the first component of w, that is w inter |X| if |X| and |Y| are assumed to be disjoint, and similarly for w2). One checks that qD(XxY)=qD(X)xqD(Y) (usual order theoretic product) up to a canonical isomorphism. And C(XxY) is the largest state coherence (wrt inclusion) making the two projections strongly stable. The "plus" is defined by duality. The exponential "!": |!X| is the set of all finite elements of qD(X), and G(X) is the restriction of C(X) to |!X|. And the exponential "?" is defined by duality. Then one proves that ! is a comonade, and that !(XxY)=(!X)tens(!Y), so that the co-Kleisli category of ! is cartesian closed. This co-Kleisli category is equivalent to the category of hypercoherences and strongly stable functions ( qD((!X)-oY) is the domain of all traces of strongly stable functions from X to Y). It is actually a full sub-CCC of the category of qualitative domains with coherence we defined in our LICS91 paper. Specifically, this means that C((!X)-oY) is the greatest possible state coherence on qD((!X)-oY) such that the evaluation function qD((!X)-oY)xqD(X)->qD(Y) be strongly stable. If E is a coherence space, let us define a hypercoherence H(E) as follows: |H(E)|=|E| and u in G(H(E)) iff u is a finite and non-empty subset of |E| which is either a singleton or contains at least two strictly compatible elements of |E| (that is, iff u is a singleton or is not in the orthogonal of the coherence space E). Then one checks that qD(H(E))=E and that C(H(E))=CL(E). So, according to the observation stated at the beginning of this note, a function from E to F is sequential iff it is strongly stable from H(E) to H(F). One can also observes that H(ExF)=H(E)xH(F) (the sign "x" does not have the same significance on both sides of this equation), so that the category of coherence spaces and sequential functions is a sub-cartesian category of the category of hypercoherences and strongly stable functions. (The category of coherence spaces and sequential functions is cartesian but not cartesian closed.) So, in some sense, strong stability is a "conservative extension" of sequentiality to higher order. In the MSCS paper, we develop also some simple considerations about a notion of "polarity" which seems to make sense in this new framework. Some additional work has also be done for comparing strongly stable functions between hypercoherences with sequential algorithms between "sequential structures" (a slight extension of CDS's), and it appears that, in some sense, the notions are equivalent. Thomas Ehrhard e-mail: ehrhard@dmi.ens.fr Return-Path: <@Sunburn.Stanford.EDU,@s.ms.uky.edu,@ms.uky.edu:radek@ms.uky.edu> To: linear@cs.stanford.edu Subject: LL and databases Date: Sat, 20 Feb 93 18:24:24 EST From: radek@ms.uky.edu Sender: lincoln@cs.stanford.edu --text follows this line-- >applications to databases sound as if it could be interesting to >more than just Radek. Perhaps replies should be broadcast to >the whole net. > Thomas Forster I will wait for more responces for a few days and then I would post all the responces received so far on the mailing list. If some of the respondents disagree with having their mails to be posted, please let me know. Radek Vingralek Return-Path: <@Sunburn.Stanford.EDU:engberg@daimi.aau.dk> From: Uffe Engberg To: linear@cs.stanford.edu Subject: Completeness results for linear logic on petri nets Date: Mon, 22 Feb 1993 10:56:54 +0100 Sender: lincoln@cs.stanford.edu --text follows this line-- We would like to announce the following new results: Uffe~Henrik Engberg and Glynn Winskel. Completeness results for linear logic on petri nets. Submitted to MFCS'93, Gda{\'{n}}sk, Poland, August 30 - September 3, 1993. Full version will appear as DAIMI PB, January 1993. Abstract: Completeness is shown for several versions of Girard's linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with $\otimes$, $\mathbin{-\mkern-3mu\raise-.21ex\hbox{$\lhook\mkern-3mu\rhook$}}$, $\vphantom{\oplus}\raisebox{-1.15pt}{\rm\&}$, $\oplus$ and the exponential ${!}$ (``of course''), and forms of second-order quantification. This logic is shown sound and complete with respect to {\em atomic nets} (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed. A dvi or postscript version of the paper can be obtained by anonymous ftp from daimi.aau.dk in the directory pub/Linear-Logic. In the same dircetory there is a dvi and a postscript version of the CAAP'90 paper: Uffe~Henrik Engberg and Glynn Winskel. Petri Nets as Models of Linear Logic. In {\em CAAP' 90, Coll.\ on Trees in Algebra and Programming (Copenhagen)}, pages 147--161. Springer-Verlag ({\it LNCS\/} 431), 1990. Abstract: The chief purpose of this paper is to appraise the feasibility of Girard's linear logic as a specification language for parallel processes. To this end we propose an interpretation of linear logic in Petri nets, with respect to which we investigate the expressive power of the logic. Below you will find a typical ftp session. If you have problems or questions, please do not hesitate to contact us. Glynn Winskel Uffe Henrik Engberg Computer Science Department Computer Science Department Aarhus University Aarhus University Ny Munkegade Ny Munkegade DK-8000 Aarhus C DK-8000 Aarhus C Denmark Denmark Email: gwinskel@daimi.aau.dk Email: engberg@daimi.aau.dk > ftp daimi.aau.dk Connected to daimi. 220 daimi FTP server (SunOS 4.1) ready. Name (daimi.aau.dk:engberg): anonymous 331 Guest login ok, send ident as password. Password: 230 Guest login ok, access restrictions apply. ftp> cd pub/Linear-Logic 250 CWD command successful. ftp> ls 200 PORT command successful. 150 ASCII data connection for /bin/ls (130.225.16.59,1158) (0 bytes). README caap90.dvi.Z caap90.ps.Z mfcs93sub.dvi.Z mfcs93sub.ps.Z 226 ASCII Transfer complete. 68 bytes received in 0.2 seconds (0.34 Kbytes/s) ftp> get mfcs93sub.dvi.Z 200 PORT command successful. 150 ASCII data connection for mfcs93sub.dvi.Z (130.225.16.59,1155) (35827 bytes) . 226 ASCII Transfer complete. local: mfcs93sub.dvi.Z remote: mfcs93sub.dvi.Z 36010 bytes received in 0.48 seconds (73 Kbytes/s) ftp> 221 Goodbye. uncompress mfcs93sub.dvi.Z