On strong normalization and type inference in the intersection type discipline

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 -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 -calculus) that typability implies weak normalizability. We then show that the unification process whic...

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Gérard Boudol
• Keywords: Intersection Type Discipline, Strong Normalization, TCS 2008, Theoretical Computer Science, Type Inference