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.