A new type assignment for λ-terms

In the present paper we propose a new type assignment for λ-terms whose motivation is to introduce a system with simple inferential rules to study termination (i.e. the property of having a normal form) of λ-terms. The main results that will be proved in this paper are:a)all λ-terms in normal form possess a type,b)all λ-terms which possess a type reduce to normal form.