One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the representation of computations and the resulting functional programming languages on the one hand and the representation of reasoning and the resulting systems of computer mathematics on the other hand.

Inside a combinatory algebra, there are ‘internal’ versions of the finite type structure over ω, which form models of various systems of finite type arithmetic. This paper compares internal representations of the intensional and extensional functionals. If these classes coincide, the algebra is called ft-extensional. Some criteria for ft-extensionality are given and a number of well-known ca's are shown to be ft-extensional, regardless of the particular choice of representation for ω. In particular, DA, Pω, Tω, Hω and certain D∞-models all (...) share the property of ft-extensionality. It is also shown that ft-extensionality is by no means an intrinsic property of ca's i.e., that there exists a very concrete class of ca's—the class of reflexive coherence spaces—no member of which has this property. This leads to a comparison of ft-extensionality with the well-studied notions of extensionality and weak extensionality. Ft-extensionality turns out to be completely independent. (shrink)