Intersection Types a la Church

In this paper, we present Λt∧, a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between Λt∧ and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable.