% -*-LaTeX-*-

\addcontentsline{toc}{author}{J. B. Wells}
\addcontentsline{toc}{chapter}{Introduction: Workshop on Intersection Types and Related Systems (ITRS 2000)}
\thispagestyle{plain}
\Headright{Introduction}
\title{Introduction:\\
Workshop on Intersection Types and Related Systems (ITRS 2000)}

The first international Workshop on Intersection Types and Related
Systems (ITRS 2000) was held in Geneva, Switzerland on 15 July 2000.
The workshop was co-located with the 27th International Colloquium on
Automata, Languages, and Programming (ICALP 2000).
For additional information about ITRS 2000, see
\url{http://www.cee.hw.ac.uk/~jbw/itrs/itrs00/}.

\section{Motivation}

The ITRS 2000 workshop brought together researchers working on both
the theory and practice of systems with intersection types and related
systems (e.g., union types, refinement types, etc.).
Types support reliable reasoning in such areas as programming
languages, logic, linguistics, etc.
A \emph{polymorphic} type is one that stands for some number of
instance types.
Using type systems for non-trivial purposes generally requires
polymorphism.

Intersection types, introduced roughly twenty years ago independently
by Coppo and Dezani~\cite{Cop+Dez-Cia:NDJFL-1980-v21n4} and
Pottinger~\cite{Pottinger:HBC-1980}, provide type polymorphism by
listing type instances.
This differs from the more well known $\forall$-quantified types,
which are polymorphic type schemes that can be instantiated into
various type instances.
(A similar relationship holds between union types and
$\exists$-quantified types, the duals of intersection types and
$\forall$-quantified 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 list of topics below).
Recent research has made a number of breakthroughs in the use of
intersection types (and similar technology) for practical purposes
such as program analysis.

\section{Program}

ITRS 2000 had two excellent invited speakers: Mariangiola Dezani, one
of the co-inventors of intersection types, and John Reynolds, one of
the co-inventors of the typed lambda calculus with
$\forall$-quantified types.
The invited talks were:
\begin{quote}
  \newcommand{\itrsspeakerinstitutiontitle}[3]
    {\begin{tabular}[t]{@{}l@{}}#1\\\hbox{}\rlap{\emph{#3}}\end{tabular}&(#2)}
  \noindent
  % TeX voodoo.  This is the only way to get real control of the
  % interrow vertical spacing in LaTeX arrays/tables.  Using struts
  % just is too painful.  Why LaTeX doesn't support this directly is a
  % mystery.
  \newcommand{\nextarrayminrowskip}[1]
    {\let\realhalign=\halign
     \DeclareRobustCommand{\halign}
       {\lineskip=#1%
        \lineskiplimit=#1%
        \let\halign=\realhalign
        \halign}}
  \nextarrayminrowskip{1ex}
  \begin{tabular}{@{}l@{\quad}l}
    \itrsspeakerinstitutiontitle
      {Mariangiola Dezani-Ciancaglini}
      {Universit{\`a} di Torino, Italy}
      {Intersection Types and Properties of Lambda Terms}
  \\
    \itrsspeakerinstitutiontitle
      {John Reynolds}
      {Carnegie Mellon University, USA}
      {An Intrinsic Semantics of Intersection Types}
  \end{tabular}
\end{quote}
There were also 7 very interesting contributed talks in such areas as
program analysis, denotational semantics, and logic.
Papers had been solicited in the following areas:
\begin{itemize}
\item
  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.
\item
  Results for clearly related systems, e.g., systems with union
  types, refinement types, or singleton types.
\item  
  Connections with not-so-clearly related approaches such as
  abstract interpretation and contraints.
\item  
  Applications to lambda calculus and similar systems, e.g.,
  denotational semantics, analysis/synthesis of lambda models
  (domains), characterization of operational properties, etc.
\item  
  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. 
\item  
  \label{itrs-topics-item6}
  Applications for other areas, e.g., database query languages, 
  program extraction from proofs, type systems for natural
  languages.
\end{itemize}
I am happy to report that the accepted papers cover all of these
topics except for item~\ref{itrs-topics-item6}.

\section{Acknowledgements}

In my role as organizer of ITRS 2000, I first want to thank
Mariangiola Dezani, Simona Ronchi Della Rocca, and Adriana Compagnoni
for their organizational advice.
The various conference organizers who I approached regarding the
possibility of co-location were extremely helpful.
The ICALP 2000 conference and its organizer, Jos{\'e} Rolim
(Universit{\'e} de Geneve), have been very supportive.
Thanks also go to Steve Izma, the editor at Carleton Scientific
handling the proceedings, for his efforts in dealing with various
thorny issues.

I also want to thank the members of program committee and their
anonymous subreviewers for donating their time to ITRS 2000 and for
doing an excellent job of reviewing the submissions and suggesting
improvements.
The program committee members are:
\begin{quote}
  \noindent
  \begin{tabular}{@{}l@{\quad}l}
     Adriana Compagnoni        & (Stevens Institute of Technology, USA)
  \\ Maribel Fern{\'a}ndez     & ({\'E}cole Normale Sup{\'e}rieure, France)
  \\ Thomas Jensen             & (IRISA/CNRS, Rennes, France)
  \\ Jean-Louis Krivine        & (Universit{\'e} Paris 7, France)
  \\ Jens Palsberg             & (Purdue University, Indiana, USA)
  \\ Simona Ronchi Della Rocca & (Universit{\`a} di Torino, Italy)
  \\ Betti Venneri             & (Universit{\`a} di Firenze, Italy)
  \\ Joe Wells (Chair)         & (Heriot-Watt University, Edinburgh, Scotland)
  \end{tabular}
\end{quote}

And of course, I want to thank the many researchers whose research in
the ITRS area has contributed to making this an exciting and
fascinating field.
Special thanks go to those who submitted papers to ITRS 2000 and those
who gave talks at ITRS 2000.

\begin{flushright}
     Joe Wells
  \\ ITRS 2000 Organizer
  \\ ITRS 2000 Program Committee Chair
  \\ June 2000
\end{flushright}
