Intersection Types and Termination Properties

Issue title: Intersection Types and Related Systems (ITRS)

Article type: Research Article

Authors: Koletsos, George

Affiliations: National Technical University of Athens, Department of Computer Science, Zografou Campus - 157 80 Athens - Greece. koletsos@math.ntua.gr

Note: [] This work was partially supported by Grant ΠEBE - 2009 from the Research Committee of the Technical University of Athens.

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.

DOI: 10.3233/FI-2012-775

Journal: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 185-202, 2012