30th SPRING SCHOOL THEORETICAL COMPUTER SCIENCE 24 - 29 March, 2002 in AGAY (VAR, FRANCE) EARLY REGISTRATION [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 IMFORMATION & EARLY REGISTRATION An early registration form can be filled at the following web address : 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