On Type Inference in the Intersection Type Discipline

We introduce a new unification procedure for the type inference problem in the intersection type discipline. We show that unification exactly corresponds to reduction in an extended λ-calculus, where one never erases arguments that would be discarded by ordinary β-reduction. We show that our notion of unification allows us to compute a principal typing for any strongly normalizing λ-expression.