Strong Normalization and Typability with Intersection Types
Silvia Ghilezan · Notre Dame Journal of Formal Logic · 1996
A simple proof is given of the property that the set of strongly normalizing lambda terms coincides with the set of lambda terms typable in certain intersection type assignment systems.van Bakel [15]).The idea that strongly normalizing lambda terms are exactly the terms typable in the intersection type assignment systems without the (ω)-rule first appeared in [4], Pottinger [11], and Leivant [10].Further, this subject is treated in [15], [9], and Ronchi della Rocca et al. [12], with different approaches.We shall present a modified proof of this property and compare it with the proofs mentioned above.Section 2 is an overview of the systems considered.In Section 3 we shall present a proof à la Tait of strong normalization for D and D ≤ based on the proof of strong