The lecture was held within the framework of the Hausdorff Trimester Program: Types, Sets and Constructions.
Kleene’s original notion of realizability (1945) makes use of all (partial) computable functions as potential realisers. Later Kreisel (1959) presented a “modified” notion of realizability based on (total) primitive recursive functionals, in the style of Gödel’s Dialectica interpretation. A natural question to ask is whether one can also go to the other way, and have a Dialectica-like version of Kleene’s original realizability, which works with all partial computable functions. This has been attemped by Beetson (1978) in a paper entitled “A type-free Gödel interpretation” (JSL). In this talk I’ll point out a mistake in Beeson’s interpretation, and suggest an alternative solution to this problem.