Program

Schedule

	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

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.
   slides

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.
   slides

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.
   slides

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.
   slides

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.
   slides

Contributed Talks

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

• Tuesday afternoon
  • Pierre-Marie Pedrot: Double-glueing: refining models of LL through realizability
    Double-glueing is a powerful abstract and categorical technique inspired from realizability. This framework has proven itself a worthy reverse-engineering of famous linear logic models from the litterature. Indeed, well-known models such as coherent spaces, phase semantics and finiteness spaces can be reduced to the composition of double-glueing and double-orthogonality closure over rawer structures. We will present this whole construction in a formal way, while relating it to aforementioned models. Although double-glueing is a purely categorical framework, we will stick to a simple approach. We will also underline the efficient cases of orthogonality and the caveats of this formalism.
    slides

  • Dominique Duval: States and exceptions considered as dual effects
    Joint work with J.-G. Dumas, L. Fousse and J.-C. Reynaud. In this talk I will present a surprising result: there exists a symmetry between the computational effects of states and exceptions, based on the well-known categorical duality between products and coproducts. More precisely, the lookup and update operations for states are respectively dual to the throw and catch operations for exceptions. This approach gives rise to a new point of view on states and exceptions, which bypasses the problems due to the non-algebraicity of handling exceptions. This talk is based on the paper http://arxiv.org/abs/1001.1662 (v4)
    slides

  • Tom Hirschowitz: Strategies as presheaves and interactive equivalences for CCS
    Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner's CCS. We construct a category E of plays, and a subcategory V of views. We argue that presheaves on V adequately represent innocent strategies, in the sense of game semantics. We then equip innocent strategies with a simple notion of interaction. This results in an interpretation of CCS. Based on this, we propose a notion of interactive equivalence for innocent strategies, based on right Kan extension along the inclusion of V into E, which is close in spirit to Beffara's realisability interpretation of testing equivalences in concurrency theory. In this framework we prove that the analogues of fair and must testing equivalences coincide, while they differ in the standard setting. This is joint work with Damien Pous.

• Thursday afternoon:
  • Federico Aschieri: Learning-Based Classical Realizability for Second Order Intuitionistic Arithmetic with EM1 and SK1
    We introduce a learning-based classical realizability for second order Heyting Arithmetic HAS with EM1 and SK1. With EM1 and SK1 we denote respectively the excluded middle and Skolem axioms over sigma_01 formulas with natural number parameters. The work extends to the second order our realizability for HA + EM1 + SK1. Realizers are written in System F plus an oracle symbol. Realizers learn oracles value in an efficient way in order to interpret constructively classical theorems. Note: joint work with Stefano Berardi.

  • Mauricio Guillermo: Specifying Peirce's law in classical realizability
    This paper deals with the specification problem in classical realizability (such as introduced by Krivine) which is to characterize the universal realizers of a given formula by their computational behavior. After recalling the framework of classical realizability, we present the problem in the general case and illustrate it with some examples. In the rest of the paper, we focus on Peirce's law, and present two game-theoretic characterizations of its universal realizers. First we consider the particular case where the language of realizers contain no extra instructions such as 'quote'. We present a first game G0 and show that the universal realizers of Peirce's law can be characterized as the uniform winning strategies for G0 , using the technique of interaction constants. Then we show that in presence of extra instructions such as 'quote', winning strategies for the game G0 are still adequate but no more complete. For that, we exhibit an example of a wild realizer of the Peirce's law, that introduces a purely game-theoretic form of backtracking that is not captured by G0 . We finally propose a more sophisticated game G1 , and show that winning strategies for the game G1 are both adequate and complete in the general case, without any further assumption about the instruction set used by the language of classical realizers.
    slides

  • Guilhem Jaber: Realizability semantics of guarded recursion
    This talk presents a (higher-order) logic where we can define guarded recursive kinds, and proves its coherence using realizability and forcing methods. This is for example crucial in the definition of kripke logical relations for languages with higher-order states, where the well-foundedness of such recursive constructions is ensured by the so-called method of step-indexing. In a recent article, Birkedal et al. have proposed to use the topos of trees to build a model of such a logic with recursive kinds. With N. Tabareau, we have developed a different approach where forcing translations of both propositions and kinds are used to prove the coherence of the logic, coming down to the ground logic where recursive constructions are not present. Finally, we will see that the forcing method can be seen as an internalization of the sheaf model inside the logic.
    slides

• Friday morning:
  • Wouter Stekelenburg: Realizability Categories and Regular Functors
    The category of assemblies for Kleene's first model has a universal property that helps us to construct regular functors from the category of assemblies to other regular categories and the construction of the category of assemblies can be generalized in a way that preserves this property.

  • Lionel Rieg: The Static Debugger : classical realizability rescuing the programer
    Software certification aims at proving the correctness of programs but in many cases, the use of external libraries allows only a conditional proof: it depends on the assumption that the libraries meet their specifications. In particular, a bug in these libraries might still impact the certified program. In this case, the difficulty that arises is to isolate the defective library function and provide a counter-example. In this talk, I will show that this problem can be logically formalized as the construction of a Herbrand tree for a contradictory universal theory. The solution I propose is based on a classical proof of Herbrand's theorem in the proof assistant Coq. Using Miquel's extension to (part of) CIC of Krivine's classical realizability for PA2, we can translate this proof into a lambda-c term through classical program extraction. The classical extraction technique in the decidable case then allows this certified program to effectively compute Herbrand trees. Using this tree and calls to the library functions, we are able to determine which function is defective and explicitly produce a counter-example to its specification.
    slides

  • Mohamad Ziadeh: Completness for simply typed lambda mu calculus
    Between the important thing, when we deal with a type or a formula A of a system of typing that satisfies the strong normalization S.N., is to build a set of terms that satisfies 'a term in the set corresponding to A is equivalent to say that t is of type A. Unfortunally it is impossible to have this equivalency because of S.N., so the work take another formulation to escape this problem and it becomes 'a term in the set corresponding to A is equivalent to say that t is in relation with t' which is of type A'. many studies having this form where been published for many systems and relations. My work will be around the simply typed system in lambda mu calculus.

  • Christophe Raffalli: why it the extensional choice hard to realize
    After recalling the realization of the non-extensional choice using the quote instruction, we will explore some possibilities for the extensional choice ... and see that this is hard.

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.