ITRS 2002

Intersection Types and Related Systems
Copenhagen, Denmark, July 26th, 2002
Affiliated with LICS 2002

Types support reliable reasoning in many areas such as programming languages, logic, linguistics, etc. A polymorphic type is one that stands for some number of instance types. The use of type systems for non-trivial purposes generally requires type polymorphism.

Intersection types, which were introduced roughly twenty years ago, provide type polymorphism by listing type instances. This differs from the more widely used universal 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.)

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 (see possible topics below). Recently, there have been a number of breakthroughs in the use of intersection types (and similar technology) for practical purposes such as program analysis.

Possible topics for submitted papers include, but are not limited to:

  • Formal properties of systems with intersection types: principal typings, normalization properties (for normal forms, head-normal forms, weak head-normal forms, etc.), type inference algorithms.
  • Results for clearly related systems, e.g., systems with union types, refinement types, or singleton types.
  • Connections with not-so-clearly related approaches such as abstract interpretation and constraints.
  • Applications to lambda calculus and similar systems, e.g., denotational semantics, analysis/synthesis of lambda models (domains), characterization of operational properties, etc.
  • Applications for programming languages, e.g., program analysis (flow, strictness, totality, etc.), accurate type error messages, increased flexibility with static typing, separate compilation and modularity, optimizing transformations, types for objects, etc.
  • Applications for other areas, e.g., database query languages, program extraction from proofs, type systems for natural languages.

Workshop web page with further information

Invited speaker

Program Committee