On strong normalization in the intersection type discipline: (Extended abstract)

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 λ-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. © Springer-Verlag Berlin Heidelberg 2003.