To start, I will give an introduction to the categorical approach to Krivine realizability, and in particular explain how Krivine realizability gives rise to toposes using Hyland, Johnstone and Pitts' "tripos-to-topos construction". Krivine realizability is parametric over the concept of "pole", and I will explain how to obtain new poles by augmenting the syntax with side effects for I/O. To conclude I will discuss potential links to algorithmic complexity theory, based on work in progress in collaboration with Jakob Grue Simonsen.

__This talk will be given in Salle des Thèses, ground floor__ (we will be in Amphi B in the afternoon).