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

Check the updatedLOCAL
INFORMATION
To check the PRELIMINARY TIMETABLE
Check also the contents of the lectures
and of the thematic sessions
(last update: 17/8/2000)
The LINEAR TMR research network "Linear Logic in Computer Science" (http://iml.univmrs.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:
The school lasts one week and comprises both lectures and thematic sessions. The lectures are in the tradition of summer schools and cover one topic, from basic material to more advanced issues. The thematic sessions will cover stateoftheart research in Linear Logic. Each session has an organizer responsible for inviting speakers who will talk about their work.JeanYves 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
JeanYves 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 ProofNets and LambdaCalculus
Proofnets 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 proofnet 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 proofnet equates sequent derivations that differ because of useless permutations of rules.Proofnets 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 proofnet by topological means only  e.g., by means of the DanosRegnier correctness criterion or by Girard's long trip criterion.
We shall start by analyzing the basic definition of proofnet 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 proofnet.
We shall discuss the connections between IMLL (intuitionistic MLL) and MLL; in particular, we shall define IMLL proofnets and we shall see the trip translation of an MLL proofnet into an IMLL proofnet.
We shall analyze the computational complexity of proofnet correctness and sequentialization algorithms; in particular, we shall see that both these problems can be solved in linear time.
Finally, since the lambdacalculus can be encoded into the multiplicativeexponential fragment of LL (MELL), we shall introduce boxes and define MELL proofnets. Therefore, we shall give a translation of typed lambdaterms into MELL proofnets and we shall see how to encode the untyped lambdacalculus into the socalled pure proofnets.
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 prooftheoretical results: cut elimination for LL (Okada);
 decidability of Affine LL (first proved by Kopylov);
 NPcompleteness 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 LogicWe hope to cover the following topics:
Lecture 2: Monoidal Structures I
Lecture 3: Monoidal Structures II
Lecture 4: GoI Categories
Lecture 5: Full Completeness1. Categories, Functors, AdjointsReferences
2. Categorical Proof Theory
3. Cartesian and cartesian closed categories
4. 2categories, strictness, multicategories, etc
5. Symmetric monoidal closed categories
6. Monoidal functors
7. *autonomous categories
8. Comonads and Comonoids
9. Chu and Loader
10. Noncommutativity: HopfAlgebras
11. Traced Monoidal Categories
12. GoI Categories
13. Full Completeness and Representation Theorems 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 LogicThe talk will be divided in 3 parts:1 Presentation of the "Linear Object" (LO) model of multiagent computation
* proof search in sequent systems
* the Focussing property in Linear Logic
* LinLog2 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 xSLAMstyle: challenges and progressThe 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 proofnetsWe will review and compare some of the techniques proposed in the literature for the local reduction of proofnets (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 logicOlivier Laurent (Marseille) Polarized linear logic, classical logic and lambdamu calculusJim Laird (Edinburgh and Brighton) Fundamental of games for classical logicRussel Harmer (Paris) Architectures of HO games models
Thomas Ehrhard Semantics
Nuno Barreiro (Lisbon) About the exponentials in coherence semanticsIn 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 JeanYves Girard, we give a characterization of the morphisms of the coKleisly 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 semanticsWe 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 extensionalityPCFprograms may be interpreted as functions on domains (eg. stable functions on dIdomains) 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 gametheoretic 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 PCFtype $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}$.PierreLouis Curien (by Thomas Ehrhard) (Paris) BistructuresBistructures are a generalisation of event structures which allow a representation of spaces of functions at higher types in an orderextensional 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 ProcessesTogether 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 builtin 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 openmap 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 ParallelismInteraction 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 cutelimination for linear logic proofnets. Together with an adequate translation of the lambdacalculus into proofnets, one may thus obtain an implementation mechanism for the lambdacalculus.We will then give an overview of the possibilities of parallel reduction of interaction nets. We will look at some implementation principles for sharedmemory and distributed memory architectures, for which we use respectively threads and messagepassing as the underlying models. The last part of the talk will address a specific implementation for interaction nets, based on a sharedmemory 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)Fees for accompanying persons are also available. They include accomodation and full board.Double room: 120000 PTE (~ 600 euros)
Accompanying person in a single room: 150000 PTE (~ 750 euros)If you have any particular requirements please contact us.Accompanying person sharing a double room: 100000 PTE (~ 500 euros)
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
Any comments on this page may be kept to yourself...