**Abstract:**

We introduce a new unification procedure for the type inference
problem in the intersection type discipline. It is well known that
type inference in this case should succeed exactly for the strongly normalizing
expressions. We give a proof for the strong normalization result in
the intersection type discipline, which we obtain by putting together
some well-known results and proof techniques. Our proof uses a variant
of Klop's extended lambda-calculus, for which it is shown that
strong normalization is equivalent to weak normalization. This is
proved here by means of a finiteness of developments theorem, obtained
following de Vrijer's combinatory technique. The main property of this
extended calculus is uniformity, i.e. weak and strong
normalizability coincide. The strong normalizability result is therefore
a consequence of the fact, first established by Coppo and Dezani (for
the lambda-calculus) that typability implies weak normalizability.
We then show that the unification process which is the
basis for type inference exactly corresponds to reduction in the
extended lambda-calculus. Finally we show that our notion of unification
allows us to compute a principal typing for any typable
lambda-expression.

[pdf]