On strong normalization and type inference in the intersection type discipline

AbstractWe 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 λ-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 normalizabilities coincide. The strong normalizability result is therefore a consequence of the fact, first established by Coppo and Dezani (for the λ-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 λ-calculus. Finally we show that our notion of unification allows us to compute a principal typing for any typable λ-expression