Non-idempotent intersection types for the Lambda-Calculus.

This article explores the use of non-idempotent intersection types in the framework of the $\lambda$-calculus. Different topics are presented in a uniform framework: head normalization, weak normalization, weak head normalization, strong normalization, inhabitation, exact bounds and principal typings. The reducibility technique, traditionally used when working with idempotent types, is replaced in...