This page



  • The morning session on Tuesday is from 10'00 am to 1'00 pm
  • other morning sessions are from 9'00 am to 12'30 am
  • afternoon sessions are from 2'00 pm to 5'30 pm,
  • each contributed talk is about 45 minutes long (including questions), followed by a break.
Morning Afternoon
Tuesday Invited course (John Longley) contributed talks
Wednesday Invited course (John Longley) Invited lecture (Stefano Berardi)
Thursday Invited lecture (Olivier Laurent) contributed talks
Friday contributed talks

All lectures and talks will take place in Amphithéatre Revard (in red on the map).

Invited Course

John Longley will give the invited course.

This course of four lectures (1.5 hours each) will present some of my own interests within the field of realizability. In the first lecture I shall try to give an overview of the entire field, but the remaining lectures will be very much slanted towards my own personal perspective: the idea of realizability as a tool for classifying and studying different "notions of computability".

  1. The many faces of realizability. A broad overview of the history of realizability and its applications to logic, type theory and semantics.


  2. Realizability over computability structures. I will present some recent work on a general framework for the `category of assemblies' construction that encompasses a wide range of models of computation from across computer science.


  3. Realizability of functionals of higher type. In many realizability models one may consider type structures of (total or partial) computable functionals over the natural numbers. In both cases, a wide range of possible realizability models leads in practice to a surprisingly small handful of distinct type structures. Furthermore, in the total case, the ideas of realizability may be used to obtain a theorem explaining why this is so.


  4. Models of sequential computation. I will review a selection of models for sequential flavours of computation, including game models and the PCF Böhm tree model. A large number of these models are found to give rise to the same class of partial functionals, namely the "sequentially realizable functionals", whose main properties and characterizations I will review.


Invited Talk

  1. Olivier Laurent will give an invited talk.
    • Games out of classical realizability

      In his classical realizability framework, Jean-Louis Krivine introduces a game interpretation of formulas characterising provability in classical first-order logic.

      The propositional intuitionistic restriction of this game can be refined to have a precise correspondence between winning strategies and proofs (in a variant of the sequent calculus). We show how this refinement directly leads to traditional Hyland-Ong games for the simply typed lambda-calculus.

      Building on this bridge between Krivine's game interpretation with realizability and game semantics, we define an Hyland-Ong-style game model for first-order classical logic.

    • Bi-orthogonality applied to games

      Orthogonality constructions are at the heart of both Jean-Louis Krivine's classical realizability and many denotational models of Jean-Yves Girard's linear logic. Double glueing and orthogonality categories give a general categorical framework abstracting these orthogonality/realizability approaches.

      After a description of the categorical setting, we will present an application to games allowing to prove important properties such as the preservation of totality under composition (and others depending on different choices of orthogonality relations).

  2. Stefano Berardi will give an invited talk.

    From a constructive mathematical proof of the existence of an individual with a given property we may automatically, through a Realization Semantics extract a certified functional program computing the individual. This extraction procedure is implemented in the French proof-assistant Coq (developed by INRIA Rocquencourt).

    A proof using classical logic (say, by contradiction) may still be interpreted as a program, but in a larger language, including extra features like continuation, parallelism, non-determinism, learning (monotonic and non-monotonic). No efficient implementation of this extraction procedure yet exists.

    The challenge is to define a Realization model of parallelism and learning, in which we may interpret classical proofs as programs, and to experiment with it.


Contributed Talks

Each contributed talk is about 45 minutes long (including questions), followed by a break.

Barbecue on Wednesday evening

A barbecue is planned for Wednesday (the 15th) evening at the "Plage des Mottets":

Agrandir le plan

It should take about 20 minutes to walk there from the campus. People will start arriving there around 7pm, and the first ones should try to claim one of the barbecues for us. (First come, first served...)

Here is an updated map with the direction to the "Plage des Mottets" in orange.

Don't forget to bring your swimming suit if you are so inclined...

Check with Barbara Petit or Thanos Tsouanas for organisation details.