The LINEAR International Summer School                  (Linear Logic and Applications)                  August 30 to September 7, 2000         Hotel Terra Nostra, S.Miguel, Azores, Portugal

The LINEAR TMR research network "Linear Logic in Computer Science" (http://iml.univ-mrs.fr/LINEAR/) is proud to announce its first International Summer School on Linear Logic and Applications.

The school will be held in the island of S.Miguel, Azores, amid luxurious vegetation and hot water springs.  The entrance to the mythic kingdom of the Atlantis is believed to be located near Hotel Terra Nostra, some say at the bottom of its famous red and hot water swimming pool...

The school is directed to everyone doing postgraduate work in Computer Science or Mathematics with an interest in the field of Formal Logic and its applications. A background in Discrete Mathematics will be helpful. Applicants and participants who wish to get an overview of the subject may consult the following documents:

Jean-Yves Girard, Linear Logic, it syntax and semantics, in Advances in Linear Logic, CUP, LMSLNS 222
Vincent Danos and Roberto di Cosmo, The Linear Logic primer (draft)

Lectures

    Samson Abramsky      Game Semantics

    Jean-Yves Girard     Linear Logic and Ludics

Linear logic is presented through ludics, a novel interactive explanation of logic.

The main thesis of ludics is the sensibility to location, which induces a distinction between familiar spiritual logic (classical, intuitionistic, and... linear), in which this sensibility is limited by the use of systematic delocation, and the more general locative logic.

Locative logic refuses the familiar (and useful!) paradigms: truth (e.g. phase models), categorical models, etc... are shown to be wrong in general. As a compensation, locative logic is structurally simpler: typically the locative tensor product is strictly commutative associative etc...

    Stefano Guerrini     Proof-Nets and Lambda-Calculus

Proof-nets are a formalism for the representation of proofs introduced by Linear Logic (LL). In a sequent derivation, a proof is arranged as a tree, where each rule is a link between its sequents. A proof-net is a graph where each occurrence of a formula is a node and each rule is a link between the occurrences of its principal formulas. In this way, a proof-net equates sequent derivations that differ because of useless permutations of rules.

Proof-nets can be used to characterize the set of valid LL derivations without resorting to a sequential (or inductive) definition. In other words, let a proof structure be a graph obtained by freely combining the links corresponding to LL rules. One can verify if a given proof structure is a proof-net by topological means only - e.g., by means of the Danos-Regnier correctness criterion or by Girard's long trip criterion.

We shall start by analyzing the basic definition of proof-net for the multiplicative fragment of Linear Logic (MLL); in particular, we shall see the major correctness criteria and prove the sequentialization theorem - i.e., how to reconstruct an MLL derivation from a proof-net.

We shall discuss the connections between IMLL (intuitionistic MLL) and MLL; in particular, we shall define IMLL proof-nets and we shall see the trip translation of an MLL proof-net into an IMLL proof-net.

We shall analyze the computational complexity of proof-net correctness and sequentialization algorithms; in particular, we shall see that both these problems can be solved in linear time.

Finally, since the lambda-calculus can be encoded into the multiplicative-exponential fragment of LL (MELL), we shall introduce boxes and define MELL proof-nets. Therefore, we shall give a translation of typed lambda-terms into MELL proof-nets and we shall see how to encode the untyped lambda-calculus into the so-called pure proof-nets.

    Yves Lafont          Phase Semantics and Decision Problems

Phase semantics is for Linear Logic (in short LL) what boolean semantics is for Classical Logic. It is a semantics of provability: a formula is provable if and only if it holds in all phase models. Phase semantics provides simple arguments for various proof-theoretical results:

-    cut elimination for LL (Okada);
-    decidability of Affine LL (first proved by Kopylov);
-    NP-completeness of Multiplicative LL (first proved by Kanovich);
-    undecidability of LL (first proved by Lincoln, Mitchell, Scedrov, and Shankar);
-    undecidability of second order Multiplicative LL (Lafont and Scedrov).

In the latter case, phase semantics plays a crucial role. Furthermore, we shall see that Multiplicative Additive LL satisfies a finite model property, but not Multiplicative Exponential LL. This suggests a strategy for proving the decidability of Multiplicative Exponential LL (open problem).

This course will be introductive, assuming only basic knowledge about sequent calculus and computability theory.

    Phil Scott           Category Theory and Concrete Models

We give an introduction to categorical logic and models for linear logics. We shall illustrate general notions using a wide range of concrete models both from the mathematical as well as the logic literature. If there is appropriate time, the last two lectures will emphasize more recent work on full completeness and geometry of interaction.

Lecture 1: Categorical Logic
Lecture 2: Monoidal Structures I
Lecture 3: Monoidal Structures II
Lecture 4: GoI Categories
Lecture 5: Full Completeness

We hope to cover the following topics:

   1. Categories, Functors, Adjoints
   2. Categorical Proof Theory
   3. Cartesian and cartesian closed categories
   4. 2-categories, strictness, multicategories, etc
   5. Symmetric monoidal closed categories
   6. Monoidal functors
   7. *-autonomous categories
   8. Comonads and Comonoids
   9. Chu and Loader
  10. Non-commutativity: Hopf-Algebras
  11. Traced Monoidal Categories
  12. GoI Categories
  13. Full Completeness and Representation Theorems

References

-    J. Lambek and P. J. Scott Introduction to Higher Order Categorical Logic, Camb. U. Press, 1986: Chapters 0, 1.
-    P. Scott, Some Aspects of Categories in Computer Science Handbook of Algebra, to appear. Available by anonymous ftp.
-    R. Seely. Linear Logic, *-autonomous categories and cofree coalgebras. in: Categories in Computer Science and Logic, J. Gray and A. Scedrov, eds., Contemp. Math Vol. 92, Am. Math. Soc.
-    G. Bierman. What is a categorical model of intuitionistic linear logic? Available by anonymous ftp.

Thematic Sessions

    Andrea Asperti       Applications

    Jean Marc Andreoli Xerox Research Centre (Europe)
    Coordination middleware with Linear Logic

The talk will be divided in 3 parts:

1- Presentation of the "Linear Object" (LO) model of multi-agent computation
          * proof search in sequent systems
          * the Focussing property in Linear Logic
          * LinLog

2- Presentation of the application context: coordination middleware
          * what is a middleware (e.g. Corba, EJB)
          * what is coordination in a distributed context (transactions, messaging)
          * why dealing with coordination issues in a middleware layer.

3- Presentation of a coordination middleware tool (CLF) that exploits the LO model
          * CLF protocol
          * CLF coordinators (clients) and coordination scripting
          * CLF participants (servers)
          * Some applications developed with CLF (Work and Knowledge flow)

Valeria de Paiva Xerox Palo Alto Research Center (USA)
Linear Functional Programming xSLAM-style: challenges and progress

The prospect of Linear Functional Programming was one of the main reasons that computer scientists initially got interested in Linear Logic. But the development of Linear Functional Programming has been much more problematic than originally envisaged.

In this talk I will describe the project  xSLAM  -- The eXplicit Substitutions Linear Abstract Machine -- developed in Birmingham by Eike Ritter, myself and collaborators. The project has  developed and implemented an efficient and easy to prove correct abstract machine xLIN based on linear logic. The project's main tools are categorical semantics, in the style of Curien and Ritter and explicit substitutions, in the style of Abadi et al. I will describe our solutions to some of the basic obstacles to linear functional programming, and discuss some of the outstanding problems.

Simone Martini Universita' degli Studi di Udine (Italy)
Techniques for local reduction of proof-nets

We will review and compare some of the techniques proposed in the literature for the local reduction of proof-nets (i.e., where erasing and duplication of boxes is performed incrementally by suitable control nodes).

    Vincent Danos        Proof Theory

Harold Schellinx (Paris)
Embedding classical logic in linear logic

Olivier Laurent (Marseille)
Polarized linear logic, classical logic and lambda-mu calculus

Jim Laird (Edinburgh and Brighton)
Fundamental of games for classical logic

Russel Harmer (Paris)
Architectures of HO games models

    Thomas Ehrhard       Semantics

Nuno Barreiro (Lisbon)
About the exponentials in coherence semantics

In the coherence space semantics of linear logic, the webs of the spaces interpreting the exponentials may be defined using cliques or multicliques (multisets whose supports are cliques).  We shall start by showing that the first interpretation is the extensional collapse of the second one. Then we shall focus on the multiclique interpretation. Inspired by the quantitative semantics of Jean-Yves Girard, we give a characterization of the morphisms of the co-Kleisly category of the corresponding comonad.  It turns out that these morphisms are the convex and multiplicative functions mapping multicliques to multicliques. This characterization is achieved via a normal form theorem, which associates a trace to each such map.

Antonio Bucciarelli (Rome)
On phase semantics and denotational semantics

We show how phase semantics, which is the semantics of truth for linear logic, can also be used for defining denotational models. These new models are "non uniform" in the sense that the interpretation of a function contains informations about its behaviour on chimeric arguments (e.g. a boolean whose value is both "true" and "false"). We present in particular a non uniform version of coherence spaces which is one particular model of this new class. This is a joint work with Thomas Ehrhard.

Paul Andre' Mellie's (Paris)
Sequentiality and extensionality

PCF-programs may be interpreted as functions on domains (eg. stable functions on dI-domains) or as strategies on games (eg. sequential algorithms on concrete data structures).  The two interpretations are different in nature (static vs. dynamic) and the analysis of their relationship stands among the recurrent problems of denotational semantics.  In a landmark article of 1997, Thomas Ehrhard relates for the first time a static and a dynamic model of sequentiality: he proves that the strongly stable model of PCF (Bucciarelli, Ehrhard, 1991) is the extensional collapse of the sequential algorithm model (Berry, Curien, 1982).  The two models are related another time in (van Oosten, 1997 ; Longley, 1998), starting from the realizability point of view.

In this talk, we connect the two models starting from a game-theoretic perspective, and derive the concept of {\em coherence} from elementary considerations on games.  We proceed in three steps. First, we enrich every sequential data structure (Lamarche, 1992) with a realizability relation between plays and a set of {\em extensions}.  Then, we compute the hypercoherence space $\semhc{T}$ interpreting a PCF-type $T$ in the strongly stable model from the concrete data structure
$\semseq{T}$ interpreting $T$ in the sequential algorithm model. Finally, we characterize the sets of extensions which may be
implemented by a strategy in $\semseq{T}$, as the cliques of $\semhc{T}$.

Pierre-Louis Curien (by Thomas Ehrhard) (Paris)
Bistructures

Bistructures are a generalisation of event structures which allow a representation of spaces of functions at higher types in an order-extensional setting. The partial order of causal dependency is replaced by two orders, one associated with input and the other with output in the behaviour of functions. Bistructures form a categorical model of Girard's classical linear logic in
which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. This a joint work with Gordon Plotkin and Glynn Winskel.

    Glynn Winskel        Concurrency

Luca Cattani 
Linearity and the Semantics of Interacting Processes

Together with Glynn Winskel, I have worked at denotational models for interacting processes, with the aim of reconciling domain theory with the semantics of concurrency. We have considered a category of (generalised) domains with a built-in notion of bisimulation based on open maps.  The category of domains supports a linear type theory,  extended with lifting and  recursive types.

During these talks I will first present our category of domains, briefly recalling previous work on categorical models of concurrency and introducing open-map bisimulation. I will then show examples of models for a range of process calculi.  I will analyse the meaning of linearity in the context of interacting processes and how this may be conveniently modelled in our setting.

The presentation will be at an introductory level, assuming only some knowledge of the main ideas behind denotational semantics and linear logic together with some basics of category theory.

Jorge Sousa Pinto
Interaction Nets and Parallelism

Interaction nets, a graphical paradigm of rewriting due to Yves Lafont, is a very promising formalism for implementation on parallel architectures.  In this talk we will start by reviewing the formalism and its properties, together with examples of its use as a programming language. Then we will see how interaction nets may be used to provide local and decomposed implementations of cut-elimination for linear logic proof-nets. Together with an adequate translation of the lambda-calculus into proof-nets, one may thus obtain an implementation mechanism for the lambda-calculus.

We will then give an overview of the possibilities of parallel reduction of interaction nets. We will look at some implementation principles for shared-memory and distributed memory architectures, for which we use respectively threads and message-passing as the underlying models.  The last part of the talk will address a specific implementation for interaction nets, based on a shared-memory architecture.

Logistics

    Deadline for application

We are accepting application forms until june 15^th. Applications after this date will be considered on a first come served basis subject to availability of rooms at Hotel Terra Nostra.

    Registration fees

The registration fee includes: accommodation from 30th August to 7th September (8 nights); full board (lunch, dinner, coffee breaks, social events); working material.

Single room: 170000 PTE (~ 850 euros)

Double room:  120000 PTE (~ 600 euros)

Fees for accompanying persons are also available. They include accomodation and full board.

Accompanying person in a single room: 150000 PTE (~ 750 euros)

Accompanying person sharing a double room:  100000 PTE (~ 500 euros)

If you have any particular requirements please contact us.

    Application

To apply to the summer school you will have to fill the application form and send it to linear@di.fc.ul.pt or to the following address:

LINEAR International Summer School
Department of Informatics
Faculty of Sciences - University of Lisbon
Campo Grande
1700 LISBOA
PORTUGAL

    Grants

A limited number of grants is available. To apply for a grant you will have to fill the grant request form and send it with the application form (in the same message/letter please).

ORGANIZING COMMITTEE

Michele Abrusci (University of Rome)
Nuno Barreiro (University of Lisbon)
Jose Luiz Fiadeiro (University of Lisbon)
 
 

LOCAL ORGANIZERS (University of Azores)

Luis Gomes (coordinator)
Helia Guerra
Francisco Martins
Helena Melo Sousa
Maria Isabel Ribeiro