Martin Escardo (University of Birmingham)

Title. Computability of solutions of higher-type equations.

Abstract. Theorem: If a higher-type equation has a unique solution in
an exhaustible range of total elements, then the solution is
computable, uniformly in the data that defines the equation and in the
functional that witnesses exhaustibility.  I'll talk about the theory
and discuss some interesting examples (including exhaustible sets of
analytic functions) and some potential examples (including Peano's
theorem for existence of solutions of differential equations).  The
technical tools include Ershov-Scott domains, Kleene-Kreisel spaces,
PCF, and Scott's equilogical spaces.