Preliminary Program of the Workshop
Lectures
- Martin Hyland (homepage), Tuesday,
Wednesday and Thursday morning. Tentative program:
- Origins: Realizability for Heyting Arithmetic. Higher types. Power types. The effective topos.
- Foundations: Hyperdoctrines. Realizability Triposes. Triposes to Toposes. Geometric morphisms.
- Variations: Relative realizability. Modified realizability. Examples and case studies.
Invited Talks
- Jaap van Oosten (homepage), Wednesday
afternoon (02/06):
- A notion of homotopy for the effective topos (related
paper) : after an introduction to the effective topos (inasmuch not covered by
Martin's lecture), I'll present several subcategories of it: separated
objects (assemblies), uniform objects, projective objects, discrete objects.
The "discrete" objects were so named (by Peter Freyd, I think), because they share the property of the natural numbers object that every map to such an object from a uniform ("very connected") object, is constant. The topological analogy however (although elaborated on by Carboni), remained rather vague. The discrete objects form a well-understood, reflective subcategory of the effective topos.
In my lecture I shall show that a more concrete analogy is possible. In fact, it is possible to regard objects of the effective topos as some sort of spaces. For every object X of the topos there is an object P(X) of "paths in X", which has good properties. Discrete objects can now be redefined as "objects in which every path is constant", and the reflection: X-->X_d, from X to its discrete reflection (which is always an epimorphism) can be seen as the map which sends each x in X to the path component it belongs to. We also have a notion of homotopy, as a direct consequence of the path spaces. In fact, there is a functor from the category of pointed objects of the topos, to the category of groups, the fundamental group construction.
The path space construction satisfies the axioms of Garner and Van den Berg for "Path Object Categories", and should therefore provide interesting models of Identity types in Martin-Löf type theory.
- A notion of homotopy for the effective topos (related
paper) : after an introduction to the effective topos (inasmuch not covered by
Martin's lecture), I'll present several subcategories of it: separated
objects (assemblies), uniform objects, projective objects, discrete objects.
- Thomas Streicher (homepage),
Friday morning (02/06):
- A Synthetic Theory of Sequential Domain: the category OSA of concrete data structures and observably sequential algorithms (due to Curien et.al.) admits a universal type of which all other types appear as retracts. Thus, we can consider the realizability topos over OSA whose properties we investigate. From this we derive axioms for a Synthetic Theory of Sequential Domains in the sense of OSA.
- Forcing within Classical Realizability (slides): we show how Krivine's Classical Realizability fits into the categorical account of realizability. Every realizability structure in the sense of Krivine can be turned into an order partial combinatory algebra (opca) giving rise to a topos. We further discuss in which sense realizability and forcing are instances of a common notion. Finally we explain how forcing inside classical realizability can be reformulated as a one step construction.
Contributed Talks
Tuesday afternoon:
- 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.
- 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. - 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. - 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.)
- 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:
- 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.
-
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 http://www.pps.jussieu.fr/~frey/main.pdf. - 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 |
| 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)
|
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.
