### Reductions, intersection types, and explicit substitutions

**Speaker:**
Dan Dougherty,
Wesleyan University

Joint work with Pierre Lescanne (ENS-Lyon)
**When & Where:** 12:30pm, Monday, April 29, 2002, Room 400 AKW

**Abstract:**

Abadi, Cardelli, Curien, and Levy defined a calculus of "explicit
substitutions" to serve as a more faithful model of
implementations of the lambda-calculus. Since then a variety of
explicit substitutions calculi have been defined.

Working in a composition-free calculus of explicit substitutions
and an augmented calculus obtained by adding explicit
garbage-collection, we explore the relationship between
intersection-types and reduction.

We show that the terms which normalize by leftmost reduction and
the terms which normalize by head reduction can each be
characterized as the terms typable in a certain natural extension
of the classical system of intersection types. The relationship
between typability and strong normalization is subtly different
from the classical case: we show that typable terms are strongly
normalizing but give a counterexample to the converse.

Our notions of leftmost- and head-reduction are
non-deterministic, and our normalization theorems apply to any
computations obeying these strategies. In this way we refine and
strengthen the classical normalization theorems.

We will also briefly describe a recent extension of the
intersection-types system (in collaboration with Steffen van
Bakel, Mariangiola Dezani-Ciancaglini, and Stephane Lengrand)
which successfully characterizes the strongly normalizing terms.