Workshop on Intersection Types and Related Systems (ITRS '00)

ITRS '00 occurred on Saturday, 15 July 2000 at the University of Geneva, Switzerland. It was colocated with ICALP '00, the 27th International Colloquium on Automata, Languages, and Programming, which ran from 9 to 15 July 2000.

Important Links

• Home Page for Intersection Types and Related Systems
• Workshop Program (including links to papers and slides)
• Photograph (taken during lunch break)
• Call for Papers
• Call for Participation
• Submissions (for PC members only)

Topic and Purpose

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 '00 workshop was 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 proceedings was published by Carleton Scientific; copies were distributed at the workshop.

Program Committee

Steering Committee