(Utrecht)

In a joint paper with Eyvind Briseid and Pavol Safarik devoted to formal systems for nonstandard analysis, we introduced "Herbrand realizability", a new realizability interpretation. Although the original motivation came from nonstandard analysis, it can also be explained as a modification of Ulrich Berger's uniform arithmetic or Lifschitz' calculable numbers. The idea there is to have two types of quantifiers, one with computational content and one without, so as to have more control over how one extracts programs from proofs. One drawback (if one sees it that way) is that one is also forced to have two types of disjunction. This is precisely what is avoided in Herbrand realizability. If time permits, I will also talk about a Dialectica variant of Herbrand realizability or its categorical aspects (a "Herbrand topos").Board Room

Department of Computer Science