09:00 | Andrej Bauer (Ljubljana) Reflexive domains and coherence numbers |

10:30 | Jaap van Oosten (Utrecht) Some more on relative realizability The talk presents some results by my Ph.D. student Wouter Stekelenburg on relative realizability toposes: geometric morphisms between these toposes, and points (there are many). |

11:30 | Pino Rosolini (Genova) Remarks on realizability |

14:00 | John Longley (Edinburgh) In what 2-category do PCAs most naturally live? In my PhD thesis (1995) I introduced a category of PCAs and applicative morphisms, which allows the construction of realizability models to be made functorial and leads to a natural notion of equivalence between PCAs. This category can be seen as somewhat limited in terms the models of computation it embraces, but the ideas can be generalized in several orthogonal directions. I will describe what now appears to me to be the "most general" natural setting for these ideas - one which not only embraces a much wider range of computational models than previous attempts, but also leads to a 2-category with much better closure properties. |

15:30 | Thomas Streicher (Darmstadt) A categorical account of Krivine's classical realizability During the first decade of this millenium J.-L. Krivine has developed his "classical realizability", i.e. a realizability interpretation of classical systems. His ultimate goal is to come up with a realizability interpretation of full ZFC. For this purpose he has to use realizability structures different from PCAs since a realizability topos over a PCA is boolean if and only if the PCA is trivial. We define the notion of an Abstract Krivine Structure (AKS) and show how they can be considered as particular cases of van Oosten and Hofstra's order pcas (OCAs). Thus Krivine's classical realizability may be considered as an instance of the kind of structures considered in the categorical approach to realizability. We also make precise in which sense AKSs generalize Cohen's forcing over a poset (conditional meet-semilattice) of conditions. Finally we discuss how forcing inside classical realizability can be considered as classical realizability over a single AKS. |