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
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
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
Workshop web page with further
Steffen van Bakel <email@example.com>, Imperial
- Franco Barbanera, U Catania,
- Mario Coppo, U Turin, Italy
- Luca Roversi, U Turin, Italy
- Franklyn Turbak, Wellesley
- Pawel Urzyczyn, Warsaw U,
- Joe Wells, Heriot-Watt U, UK