Proceedings of the Third International Workshop on Intersection Types and Related Systems (ITRS 2004)

Types support reliable reasoning in many areas such as programming languages, logic, linguistics, etc. A polymorphic type stands for some number of instance types. The use of type systems for non-trivial purposes generally requires polymorphic types. Intersection types were introduced roughly twenty years ago to provide type polymorphism by listing type instances. This differs from the more widely used "forall"-quantified types, which provide type polymorphism by giving a type scheme that can be instantiated into various type instances. (A similar relationship holds between union types and existential types, the duals of intersection types and universal types.) Although intersection types were initially intended for use in analyzing and/or synthesizing lambda models as well as in analyzing normalization properties, over the last twenty years the scope of theoretical research on intersection types has broadened. Recently, there have been a number of breakthroughs in the use of intersection types (and similar technology) for practical purposes such as program analysis. The ITRS '04 workshop aims to bring together researchers working on both the theory and practice of systems with intersection types and related systems (e.g., union types, refinement types, etc.).