Strict intersection types for the lambda calculus

This paper will show the usefulness and elegance of strict intersection types for the Lambda Calculus; these are strict in the sense that they are the representatives of equivalence classes of types in the BCD-system [Barendregt et al. 1983]. We will focus on the essential intersection type assignment; this system is almost syntax directed, and we will show that all major properties hold that are known to hold for other intersection systems, like the ap-proximation theorem, the characterisation of (head/strong)normalisation, completeness of type assignment using filter semantics, strong normalisation for cut-elimination and the principal pair property. In part, the proofs for these properties are new; we will briefly compare the essential system with other existing systems