34th Spring School in Theoretical Computer Science (EPIT 2006)
Ile de Ré, from May 28th to June 2nd 2006
Organization: Paul-André Melliès (PPS) and Anca Muscholl (LIAFA)
| Samson Abramsky (Oxford, UK) | Algorithmic and Concurrent Game Semantics |
| Jacques Duparc (Lausanne, Suisse) | Describing the Complexity of ω-Languages with Games |
| Paul Gastin (LSV, ENS Cachan) | Distributed synthesis: synchronous and asynchronous semantics |
| Erich Grädel (Aachen, Allemagne) | Games and Fixed Point Logics |
| Martin Hyland (Cambridge, UK) | Games and proofs |
| Luke Ong (Oxford, UK) | Infinite trees, higher-order recursion schemes and game semantics |
| Tristan Tomala (Ceremade, Paris Dauphine) | Jeux répétés et transmission d'information |
| Igor Walukiewicz (Bordeaux) | Pushing the limits of the μ-calculus |
| Wieslaw Zielonka (Paris) | Stochastic parity games |
In less than thirty years, computer science has evolved from closed systems (the early calculators) to open systems (organized in networks). Indeed: the computer of today is far from the autonomous entity which we used to know. It is better described as a concerting community of interactive agents, each one concurrently evolving in a concurrent way. Describing and verifying the behaviour of such a "computational ecosystem" is one of the major scientific challenges of our time. It is the subject of active research today, at the interface between Computer Science and Mathematics. New conceptual tools are necessary to regulate the apparent combinatorial disorder. Developing them requires to reunderstand the classical recursivity theory (inherited from Gödel, Kleene and Turing) and to lay the mathematical foundations of the "open informatics" of tomorrow.
Game Theory is one of the most serious candidates for this refoundation. There are several reasons for that. First, this theory offers a pleasant framework in order to model the interactions between several concerting agents. Game Theory has recently taken the lead in several branches of Computer Science, from the mathematical study of programming languages (Semantics) to the specification and formal certification of concurrent programs (Verification). Finally, Game Theory is already very much studied in other parts of Computer Science and/or Mathematics, like mathematical logic, dynamical systems and economic sciences.
The Spring School will benefit the student and young researcher interested in learning the recent developments of Game Theory in the Semantics and Verification of Programming Languages.
The lectures will be introductory, and provided in a relaxed atmosphere.
Not only that: the school is openly multi-disciplinary, and internationally recognized specialists will lecture on other areas of applications of Game Theory, like mathematical logic and economy.
In both the fields of Semantics and Verification, one is interested in the behaviour of a program facing an environment. In the game-theoretic approach favoured here, the two entities, Program and Environment, are understood as two Players (or two Strategies) confronting in a game defined by the specification of the system.
In a typed programming language, every program has a type, which specifies its main properties. Interpreting the language consists in transporting the symbolic grammar of types to the algebraic grammar of games, structured in a category of games and strategies. In this way, one associates a game to every type of the language; and a strategy and a counterstrategy of the game to every program and environment of that particular type. Hence, semantics offers an algebraic framework to compute explicitly the strategies associated to a program and to its environment. By nature, semantics is modular and compositional: the semantics of a program is the product of the semantics of its components. It is thus safe to replace a component of a program by a more efficient component with the same semantics.
In this framework, specifying a program amounts to formally defining a game; whereas checking that the program satisfies the specification amounts to checking that the strategy is winning in the game defined by the specification. A more difficult question consists in synthesizing a program which would behave properly according to a given specification, whatever the behaviour of the environment. This automatic synthesis problem may be formulated in this way: one wants to compute the winning strategy in the game defined by the specification, in order to deduce the synthesized program. One also wants to control an existing program in order to satisfy a given specification (whatever the behaviour of the environment). In that case, the controler is a winning strategy which represents the valid program in the game fragment explored by the initial program.
Game semantics offers a fruitful and still largely unexplored meeting point for Semantics and Verification, two branches of mathematical computer science which diverged, alas, at the end of the 1970s. It is a sign that Verification appeared recently in Semantics when the equivalence of two programs written in Idealized Algol was reduced to deciding the equality of two rational languages. Conversely, the ideas of Semantics appeared recently in Verification in order to check software components in a modular and compositional fashion.
Hence, it is essential to bring together the best specialists of Game Theory in Semantics and Verification. The convergence of the two communities around Game Theory is a preliminary step before the emergence of a general theory of semantics and of verification of open and safe programs. The Spring School 2006 is a foundational event from that point of view. It is indeed the first national or international meeting dedicated to Game Theory, in which the two communities of Semantics and Verification will be on an equal footing. The organizers of the School represent two famous and active teams in each field. The LIAFA team is part of the European Network TMR GAMES (2002-2006) whose aim is to develop Game Theory in Verification. The PPS team is internationaly recognized for its expertise in the Semantics of programming languages based on Game Theory.
Sponsors of the Spring School 2006
This page is maintained by Samuel Mimram.
