 Spector’s (1962) functional interpretation of \(\bZ_2\) via bar recursive functionals was of great interest to proof theory. However, it was not clear whether there was a constructive foundation of these functionals along the lines of hereditarily continuous functionals that can be represented by computable functions (akin to Kleene 1959; Kreisel 1959) which would make them acceptable on intuitionistic grounds. In 1963 Kreisel conducted a seminar the expressed aim of which was to assay the constructivity of Spector’s interpretation (see Kreisel 1963). Specifically he asked whether an intuitionistic theory of monotonic inductive definitions, \(\bID^i_1(\text{mon})\), could model bar recursion, or even more specifically, formally capture a class of indices of representing functions of these functionals. In a subsequent report the seminar’s conclusion was later summarized by Kreisel: