A new type assignment for λ-terms

authors: M Coppo, M Dezani-Ciancaglini
year: 1978
url: https://doi.org/10.1007/BF02011875
publisher:
abstract: 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.