mystery logo

Preliminary Program of the Workshop

This program might change...


Invited Talks

Contributed Talks

Tuesday afternoon:

  1. Guilhem Jaber, Forcing and lambda-calculus: Following the idea of forcing, we show how we can add a generic function (i.e. a Cohen real) to lambda-calculus. Using many of them, we can compute universal quantification for predicates on the Cantor Space, and generalizing this idea, on any compact space. Presenting a proof of strong normalization for such a calculus, we will see some links with sheaf semantics. The implementation of these ideas makes great use of monadic representation of computational effects, the forcing being represented by the composition of the State and the List Monad.
  2. Andrew Swan, Realizability and Choice (slides)
    It is well known that forcing, due to Paul Cohen, can be used to show many independence results in set theory. In this talk we consider the version of realizability developed by Kreisel, Myhill, etc for set theory (IZF). We show that these techniques are similar enough to forcing, that an old result, the independence of countable choice, can be carried over, to give a new proof using only realizability.
  3. Alexandre Miquel, a computational analysis of proof transformation by forcing (slides)
    Last year, Krivine showed how to implement the method of forcing in classical realizability. Using Krivine's results as a source of inspiration, we propose to analyze the program transformation underlying forcing. For that, we will rephrase the forcing translation in (an extended version) of classical higher-order arithmetic with Curry-style proof-terms. We will define the forcing translation on propositions and higher-order terms, and show that the underlying transformation of derivations corresponds to a simple program transformation on the underlying Curry-style (raw) proof-terms. We will study the computational behavior of the transformed proof-terms, and deduce from it a new abstract machine, the KFAM (Krivine Forcing Abstract Machine), that is tailored to execute classical proofs built using the method of forcing. We shall discuss the similarities between the features of the KFAM and the notions of "protection rings", "tracing" and "virtual memory management" on which modern CPUs are based.
  4. Benno van den Berg, Herbrand realizability: In this talk, I will introduce a new type of realizability and show how it can be used to give a realizability interpretation of a system of non-standard arithmetic. (This is joint work with Eyvind Briseid and Pavol Safarik.)
  5. Federico Aschieri, Learning Based Realizability: We give an overwiew of the state of the art of learning based realizability. In particular, we present this new notion of realizability and show how it can be applied to Heyting Arithmetic plus excluded middle on Sigma_0_1 formulas, offering an interpretation of proofs as learning programs. We also discuss the relationship between learning based realizability and Coquand games and how realizers represent winning strategies in 1-Backtracking games. Moreover, we talk about foundational issues and explain how learning can be analyzed constructively, giving another constructive interpretation of Classical Arithmetic.

Friday afternoon:

  1. Mircea Hernest, Modal Functional Interpretation: We extend Goedel's Dialectica interpretation to modal formulas and prove it sound for a certain modal arithmetic based on Goedel's T. The range of this Modal Dialectica interpretation is the usual Heyting Arithmetic in all finite types HA^omega. We illustrate the use of the new tool for optimized program synthesis as part of an enhanced light Dialectica interpretation in the sense of Hernest & Trifonov.
  2. Jonas Frey, A decomposition of the tripos-to-topos construction (slides)
    In their article [1], Hyland, Johnstone and Pitts describe how to construct toposes from triposes, and how to construct functors between the ensuing toposes from certain natural transformations between the triposes. A categorically minded person might ask for the 2-categorical nature of this construction, and in previous (unpublished) work [2], we observed that the construction is in fact oplax functorial and described a framework in which it can be characterized as a kind of left biadjoint to a forgetful functor. While our analysis provided an abstract characterization, it did not provide an easy and explicit global description of the oplax functor and the associated transformations of the adjunction, and the construction remained difficult to work with. The main reason for the arising complications is the use of `weakly complete' objects in the construction of functors from tripos transformations which have to be carried along for example when computing composition constraint cells. To resolve these problems and to explain the rule that is played by the `weakly complete objects', we describe a decomposition of the tripos-to-topos construction in two steps. The first step constructs from a tripos a category which has the same objects as the associated topos, but as morphisms not all functional relations but only those which are witnessed by an arrow in the base. The second step recovers the topos as a reflective subcategory of the intermediate category. Abstractly, the decomposition of the tripos-to-topos construction is induced by factoring the forgetful functor from toposes to triposes through an intermediate 2-category whose objects are a weakened version of quasitoposes.
    [1] J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc., 88(2):205—231, 1980.
    [2] Jonas Frey. A universal characterization of the tripos-to-topos construction.
    Master thesis, available at
  3. Wouter Stekelenburg, Points of Relative Realizability Toposes: I will discuss part of the structure of relative realizability toposes, In order to explain the properties of regular functors in general, and points in particular.

Preliminary schedule

This is still preliminary.

Morning (9'00—12'30) Afternoon (14'00—17'30)
Monday (31/05) nothing preliminary course: Tom Hirschowitz (slides)
Tuesday (01/06) invited course: Martin Hyland, I contributed talks
  • Guilhem Jaber
  • Andrew Swan (slides)
  • Alexandre Miquel (slides)
  • Benno van den Berg
  • Federico Aschieri
Wednesday (02/06) invited course: Martin Hyland, II invited talk: Jaap van Oosten
Thursday (03/06) invited course: Martin Hyland, III free (unofficial social event)
Friday (04/06) invited talk: Thomas Streicher (slides) contributed talks (only until 16'00)
  • Jonas Frey (slides)
  • Wouter Stekelenburg
  • Mircea Hernest

The program of the contributed talk will be announced later

Social Events

There is no official social event, but the following have been known to happen spontaneously:

  • restaurant on Wednesday evening: people have to register the day before, and everyone pays for his own meal.
  • Working and swimming time on Thursday afternoon: people can discuss and work together (on campus), or have a swim at the "lac du Bourget", or both.
  • barbecue on Thursday evening, at the "plage des Mottets", on the "lac du Bourget" (walking distance from the campus). The participants will have to choose their own organizing committee for that, and we'll happily help.