Sciweavers

Share
TCS
2008

On strong normalization and type inference in the intersection type discipline

8 years 5 months ago
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...
Gérard Boudol
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCS
Authors Gérard Boudol
Comments (0)
books