Computability on Continuous Higher Types and its Role in the Semantics of Programming Languages

Abstract

This paper is about mathematical problems in programming language semantics and their influence on recursive function theory. In the process if constructing computable Scott models of the lambda calculus we examine the concepts of deterministic and non-deterministic effective operators of all finite types and continuous deterministic and non-deterministic partial computable operators on continuous inputs of all finite types. These are new recursion theoretic concepts which are appropriate to semantics and were inspired in part by Scott's work on continuity.