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]