Semantics and Games

Geometry of Computation 2006

Marseille - Luminy
February 20 - 24, 2006

Context

This workshop is part of Geometry of Computation 2006 (Geocal06), a special series of events in theoretical computer science organized by the GEOCAL group and taking place at the CIRM from January 30 to March 3.

Thematic presentation

Denotational semantics explores the meaning of proofs and programs as morphisms acting on abstract mathematical spaces. The first models were based on domains (partially ordered sets) such as Scott domains, dI-domains, coherence spaces etc. and continuous or stable morphisms; recent developments in this area have led to sophisticated accounts of sequentiality (strong stability, bi-stable morphisms).

Game models interpret proofs/programs as strategies in games, providing an operationally more informative interpretation of proofs, with remarkable mathematical achievements (full completeness theorems, interpretation of statefull programming languages, a new approach to the type isomorphisms problem, etc., and also the related theory of ludics, an interactive viewpoint on logic).

New models interpret proofs as continuous linear functions on vector spaces, with possible connections to quantum programming, and operational interpretations of the Taylor formula. This workshop will be an opportunity of confrontation between these various lines of reseach, in this very active field.

Talks

Organizers

Pierre-Louis Curien and Olivier Laurent    (laboratoire Preuves Programmes Systèmes)