Non-idempotent intersection types for the Lambda-Calculus
Antonio Bucciarelli, Delia Kesner, Daniel Lima Ventura · Logic Journal of IGPL · 2017
This article explores the use of non-idempotent intersection types in the framework of the λ-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 this framework by trivial combinatorial arguments.