**Abstract:**

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. Then we use the standard argument, formalized
by Lévy as ``the creation of redexes is decreasing'' and
implemented in proofs of weak normalization by Turing, and Coppo and
Dezani for the intersection type discipline, to show that a typable
expression of the extended calculus is normalizing.

[PostScript, .ps.gz]