Essential Intersection Type Assignment

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 [15]. 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 approximation 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. Contents

• Type: Conference
• Year: 1993
• Where: FSTTCS
• Authors: Steffen van Bakel
• Keywords: FSTTCS 1993, Intersection Type, Software Engineering, Strict Intersection Types, Type Assignment