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.