CR-02 : Concurrence et complexité implicite

Programme de l’UE

On étudiera les systèmes concurrents et le calcul fonctionnel par le biais de deux formalismes: les calculs de processus d’une part, et le lambda-calcul d’autre part. Des problèmes comparables se posent pour
l’analyse des systèmes dans les deux cadres: peut-on statiquement garantir que l’exécution d’un programme va terminer ? Peut-on apporter des bornes de complexité en temps sur cette terminaison?

Dans le cas des calculs concurrents, on développera les concepts permettant de raisonner sur la dynamique des systèmes, sur l’équivalence de processus, et sur leur terminaison. Dans celui du lambda-calcul on présentera des systèmes de types dérivés de la logique linéaire et permettant de garantir statiquement des bornes de complexité sur les programmes. On illustrera ainsi comment des techniques communes (typage) peuvent être exploitées à la fois dans le cadre concurrent et dans le cadre fonctionnel.  Enfin si le temps le permet on verra comment les méthodes développées pour la complexité dans le cadre du calcul fonctionnel inspirent des approches similaires dans le cadre concurrent.

Prérequis. 

  • notions élémentaires de lambda-calcul simplement typé,
  • définitions de base de classes de complexité en temps déterministe (les notions des cours d’algorithmique de L3 sont suffisantes). Les définitions nécessaires seront cependant rappelées.

Calendrier prévisionnel : 08/10, 09/10, 16/10, 22/10, 23/10, 6/11, 12/11, 13/11, 19/11, 26/11, 27/11, 4/12

Modalités d’examen. Un devoir à la maison en cours de trimestre, et un examen écrit à la fin du cours.

Intervenants:

  • Patrick Baillot, CR CNRS (responsable)
  • Damien Pous, CR CNRS

ER-05 (2010) : Game semantics and linear logic

February, 8-12, 2010 — ENS Lyon

Lecturers :

Introduction

Linear logic was introduced by Jean-Yves Girard in 1986 as a
refinement of intuitionnistic logic. In the context of the
Curry-Howard correspondence between proofs and programs, linear logic
has renewed a lot of questions in proof theory in relation with the
semantics of programs.

Partly inspired by models of linear logic, game semantics provided in
1994 the first fully abstract model of the functional programming
language PCF. It has evolved towards the interpretation of various
additional programming features as well as applications to the
verification of programs.

These topics have evolved in two separate directions (proof theory for
linear logic, and programming semantics for game semantics) but with
many transfers of ideas between them along the past fifteen years.

Location and schedule

The lectures will take place in “amphithéatre B”, at the 3rd floor of the GN1 building (main building at 46, allée d’Italie).
Tentative schedule:

  • Monday, February 8:
    • 10:00 AM – 11:30 AM Game semantics
    • 1:30 PM – 4:30 PM Linear logic
  • Tuesday , February 9:
    • 8:30 AM – 11:30 AM Game semantics
    • 1:30 PM – 4:30 PM Linear logic
  • Wednesday, February 10:
    • 8:30 AM – 11:30 AM Game semantics
    • 1:30 PM – 4:30 PM Linear logic
  • Thursday, February 11:
    • 9:30 AM – 12:30 AM Linear logic
  • Friday, February 12:
    • 8:30 AM – 11:30 AM Game semantics
    • 1:30 PM – 3:00 PM Game semantics

On thursday, Febr. 11 afternoon, the
Choco seminar , on related topics, might also interest the participants.

Course outline

Course 1: Game Semantics with Applications [in English, 12h]

Dan Ghica (University of Birmingham)

content:

  • basic concepts of game semantics
  • the fully abstract game model of a procedural concurrent programming language
  • concrete algorithmic representations of game models
  • applications of finite-state game models to program verification
  • approximating and refining game models
  • a survey of more advanced techniques for program verification using game models
  • Geometry of Synthesis, a categorical framework for circuit design
  • extracting circuit descriptions from game semantics
  • a survey of open problems in game semantics and applications

Course 2: Linear Logic [12h]

Lorenzo Tortora de Falco (University of Roma 3)
Olivier Laurent (LIP – ENS Lyon)
content:

  • sequent calculus for linear logic (1h30, monday LTdF)
  • proof-nets (3h, monday, tuesday LTdF)
  • translations of intuitionistic and classical logics (3h, tuesday, wednesday OL)
  • the coherent model and the relational model (1h30,wednesday LTdF)
  • geometry of interaction and game semantics for linear logic (3h, thursday OL)

(LTdF: Lorenzo Tortora de Falco, OL: Olivier Laurent)

References and documents

Course 2:

  • Olivier Laurent. Théorie de la démonstration. pdf .
    pages 89-90 (section 5.3), 87-89 (section 5.2), pages 143-150 (chap. 10), pages 111-122 (chap. 7), pages 130-134 (section 8.3)
  • Samson. Abramsky. Semantics of Interaction: an introduction to Game Semantics. pdf pages 1-14.

Local contact

There are several useful informations on the main page of the research schools in Computer Science at ENS Lyon.