Home Page for Intersection Types and Related Systems

A Brief Description of Intersection Types

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 near the end of the 1970s 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 (Intersection Types and Related Systems) Workshops


The ITRS workshops are held 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.).

The Events

Steering Committee

Mariangiola Dezani-Ciancaglini  (UniversitÓ di Torino, Italy)
Joe Wells (Chair) (Heriot-Watt University, Edinburgh, Scotland)

Links to Resources Related to Intersection Types