30th SPRING SCHOOL THEORETICAL COMPUTER SCIENCE

[Ecole d'ete 2001]

=======================================================================
            30th SPRING SCHOOL THEORETICAL COMPUTER SCIENCE
               24 - 29 March, 2002 in AGAY (VAR, FRANCE)

                      PRELIMINARY ANNOUNCEMENT

                  [Apologies for multiple copies]
=======================================================================

 This spring school aims at bringing together students and researchers
eager to learn about the fundamental questions which language designers
and implementors are facing those days, and on the most up-to-date 
tools that theoreticians have developed or are in the process of 
developing (such as games and ludics, or realisability for classical 
logic and set theory).

 Denotational semantics was born some thirty years ago from the 
encounter of computer scientists who aimed at implementation
independent definitions of programming constructs on one hand, and 
logicians who provided mathematical tools to this aim (domain theory) 
on the other hand. Algebraic tools such as initial algebra semantics 
were also instrumental to the birth of this subject.

 Thirty years later, the subject has enriched considerably, both in 
tools (including connections with proof theory and category theory) and
in coverage and applications (functional programming, state, control, 
objects, parallelism, mobility,...). Concepts and constructs that have 
arisen in the design of programming languages have found counterparts 
in logic, logical systems have found their way to applications in the 
form of proof assistants, etc... The rapid development of new 
programming paradigms, in which distributed computation takes a more 
and more important part, infers a strong demand on theory, more than 
ever.

 With the rise of quite specialized subcommunities (like type theory,
linear logic, pi-calculus, functional programming, etc...), it is 
important to keep an eye on more comprehensive training events, that 
can address the interrelations between research areas in rapid growth,
and between theory-oriented research work and more goal-oriented one,
with the prospect of solving problems or of improving our understanding
in one domain using tools of another domain. The diversity of the 
proposed lectures, combined with their conceptual overall unity (as 
witnessed by the very limited number of core formal systems: 
lambda-calculus, linear logic, pi-calculus) addresses this issue.

=======================================================================
LECTURES
=======================================================================

  Denotational semantics and games semantics (5 hours) :
     Thomas Ehrhard , Guy McCusker

  Ludics (4 hours) :
     Pierre-Louis Curien, Jean-Yves Girard

  Realisability (4 hours) :
     Vincent Danos, Jean-Louis Krivine

  Continuations (4 hours) :
     Olivier Danvy

  Compilation, objects, modules (4 hours) :
     Xavier Leroy

  Mobility (5 hours) :
     Luca Cardelli, Cedric Fournet

  Security (5 hours) :
     Martin Abadi, Francois Pottier


=======================================================================
CONTACT & FURTHER INFORMATION
=======================================================================

http://www.pps.jussieu.fr/~ecole/   email: ecole@pps.jussieu.fr

Equipe Preuves Programmes et Systèmes
Université Denis Diderot
Case 7014
2 Place Jussieu
75251 PARIS Cedex 05
FRANCE