Abstract:
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 lambda-calculus, where one
never erases arguments that would be discarded by ordinary
beta-reduction. We show that our notion of unification allows us
to compute a principal typing for any strongly normalizing
lambda-expression.