Subject: New Foundations for the Geometry of Interaction (full version)
From: Samson Abramsky <[email-masked]>
To: [email-masked]
Date: Thu, 10 Dec 1992 16:03:13 +0000 (GMT)

--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:[email-masked]>
To: [email-masked]
Organization: Steklov Mathematical Institute, Moscow
From: [email-masked] (Lev D. Beklemishev)
Date: Tue,  5 Jan 93 15:48:48 +0300 (MSK)
Subject: Constant-Only LL is undecidable
Sender: [email-masked]
--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:[email-masked]>
To: [email-masked]
Organization: Steklov Mathematical Institute, Moscow
From: [email-masked] (Lev D. Beklemishev)
Date: Sun, 10 Jan 93 17:13:13 +0300 (MSK)
Subject: Complexity of Constant-Only Fragments of LL
Sender: [email-masked]
--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:[email-masked]>
Date: Tue, 19 Jan 93 14:26:43 EST
From: [email-masked] (Robert A. G. Seely)
To: [email-masked]
Subject: Coherence for weakly distributive categories
Sender: [email-masked]
--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 [email-masked] if you have any trouble with the ftp process or
with printing the files at your site.


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Sat, 23 Jan 93 23:06:57 +0100
From: Voronkov Andrei <[email-masked]>
To: [email-masked]
Subject: LPAR93 deadline extension and CFP
Sender: [email-masked]
--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 [email-masked]. 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 [email-masked].

=======================================================
\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 [email-masked]. 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 [email-masked].

\end{document}


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Mon, 25 Jan 93 13:48:28 +0100
From: [email-masked]
To: [email-masked]
Subject: Summer School in ``Logic in Computer Science''
Sender: [email-masked]
--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: [email-masked]

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 [email-masked]
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

\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 [email-masked]}
\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:[email-masked]>
To: [email-masked]
Subject: referencies inquiry
Date: Tue, 16 Feb 93 01:38:49 EST
From: [email-masked]
Sender: [email-masked]
--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    [email-masked]      [email-masked]
                   [email-masked]

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:[email-masked]>
From: Thomas Ehrhard <[email-masked]>
Subject: Hypercoherences
To: [email-masked]
Date: Fri, 19 Feb 93 12:22:07 WET
X-Mailer: ELM [version 2.3 PL11]
Sender: [email-masked]
--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: [email-masked]


Return-Path: <@Sunburn.Stanford.EDU,@s.ms.uky.edu,@ms.uky.edu:[email-masked]>
To: [email-masked]
Subject: LL and databases
Date: Sat, 20 Feb 93 18:24:24 EST
From: [email-masked]
Sender: [email-masked]
--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:[email-masked]>
From: Uffe Engberg <[email-masked]>
To: [email-masked]
Subject: Completeness results for linear logic on petri nets
Date: Mon, 22 Feb 1993 10:56:54 +0100
Sender: [email-masked]
--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: [email-masked]	Email: [email-masked]

> 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