Dag will be visiting on Monday only, hosted by Martin Escardo.

Abstract

We will consider the typed hierarchy of algebraic domains based on the flat domain representation of the natural numbers. We prove that to any total, computable functional of type three there is a total functional below it definable via a deterministic algorithm. This algorithm can be realised as a PCF-program. If time, we will discuss how this result extends to higher types.