Theory and Practice of Higher-type Computation (Tutorial)

Martin Escardó
In higher-type computation, established by Kleene and Kreisel in the late 1950's (independently), one works with the data types obtained from the discrete natural numbers by closing under finite products and function spaces. For the theory of higher-type programming languages, it is natural to work with a corresponding hierarchy, or type structure, of domains, identified by Ershov and Scott in the late 1960's (again independently). The Kleene-Kreisel and Ershov-Scott hierarchies account for total and partial...