A decidable theory of type assignment (Q365669)

This is an important, interesting and well written paper. It's contents are well described in the author's abstract which I quote: 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 [\textit{J.-Y. Girard} et al., Proofs and types. Cambridge etc.: Univ. Press (1989; Zbl 0671.68002)]. It is like the simple type 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 recusive 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 \(\epsilon_0\)-recursion which takes every typable term to a natural number which is an upper bound to the lengths of all \(\beta \eta\)-reduction sequences starting with that term.