Intersection Types and Related Systems

ITRS '02 took place on Friday, July 26 2002, in Copenhagen, Denmark. It was colocated with FLoC '02, the 2002 Federated Logic Conference, which ran from July 22 to August 1 2002.

Invited speaker

Important Links

• Home Page for Intersection Types and Related Systems
• Electronic Notes in Theoretical Computer Science proceedings.
• Workshop Programme (including links to papers)
• Call for Papers
• TeX class file

Topic and Purpose

Intersection type disciplines originated in 1980 to overcome the limitations of Curry's type assignment system and to provide a characterisation of the strongly normalising terms of the Lambda Calculus. Since then, intersection types disciplines were used in a series of papers for characterising evaluation properties and semantics.

Types also support reliable reasoning in many areas such as programming languages, logic, linguistics, etc. A polymorphic type stands for some number of instance types, and the use of type systems for non-trivial purposes generally requires polymorphic types. In this context, roughly speaking, intersection types could be seen as 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 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.).

Programme Committee

Steering Committee