Tests, games, and Martin-Löf's meaning explanations for intuitionistic type theory

Peter Dybjer

(University of Gothenburg)

In this informal talk I will present some of my latest thoughts on the connection between tests, games and the foundation of constructive logic. The starting point is Martin-Löf's meaning explanations for intuitionistic type theory which were presented in the paper "Constructive Mathematics and Computer Programming" (LMPS 1979). Martin-Löf there explains the meaning of the judgement of the theory in terms of lazy evaluation to canonical form. I essentially follow this idea but think of his meaning explanations as being about real tests of programs. This leads me to propose an alternative explanation of the meaning of higher-order functions, as passing certain kinds of interactive tests in the style of game semantics. Technically, we use the connection between Hyland-Ong games and so called PCF Böhm trees to build a model of type theory. We discuss the connection between this "meta-mathematical" model and the "pre-mathematical" tests.
Tuesday 24th September 2013, 15:00(!)
Robert Recorde Room
Department of Computer Science