Intersection Types and Termination Properties

Abstract

We use the system of intersection types and the type assignment method to prove termination properties in λ-calculus. In the first part we deal with conservation properties. We give a type assignment proof of the classical conservation theorem for λI calculus and then we extend this method to the notion of the reduction β_I and β_S of de Groote [9]. We also give a direct type assignment proof of the extended conservation property according to which if a term is β_I, β_S-normalizable then it is β-strongly normalizable. We further extend the conservation theorem by introducing the notion of β_*-normal form. In the second part we prove that if Ω is not a substring of a λ-term M then M can be typed in the Krivine's system D of intersection types. In that way we obtain a type assignment proof of the Sørensen's Ω-theorem.