Abstract

This article investigates a theory of type assignment (assigning types to lambda terms) called ETA which is intermediate in strength between the simple theory of type assignment and strong polymorphic theories like Girard’s F (Proofs and types. Cambridge University Press, Cambridge, 1989). It is like the simple theory and unlike F in that the typability and type-checking problems are solvable with respect to ETA. This is proved in the article along with three other main results: (1) all primitive recursive functionals of finite type are representable in ETA; (2) every term typable in ETA has a unique normal form; (3) there is a function defined by ${{\varepsilon}_0}$ -recursion which takes every typable term to a natural number which is an upper bound to the lengths of all βη-reduction sequences starting with that term