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.