Characterizations of the basic feasible functionals of finite type

The authors define a simple typed while-programming language that generalizes the sort of simple language used in computability texts to define the familiar numerical computable functions and corresponds roughly to the μ-recursion of R.O. Gandy (1967). This language does not fully capture the notion of higher type computability. The authors define run times for their programs and prove that the feasible functionals of S. Cook and A. Urquhart (1988) are precisely those functionals computable by typed while-programs with run times feasibly length-bounded. The authors introduce the notion of a bounded typed loop program and prove that a finite type functional is feasible if it is computable by a bounded typed loop program