On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558)

This is a survey paper whose central thesis is that Church's \(\lambda\)- calculus, rather than being one of many possible formalisms for computability theory, should be regarded as the core formal theory of computable functions and functionals. The author supports his main contention by surveying the principal connections between \(\lambda\)- calculus and three important areas in modern logic: higher type recursion theory, category theory, and proof theory. There are five sections in the paper and an extensive bibliography; the emphasis in each section is on structures invented for the semantics of typed and type-free \(\lambda\)- calculus.