Intersection types for lambda calculus and term rewriting systems

Steffen van Bakel

(University of Turin)

The type systems used for functional programmings languages are for the larger part presented as systems for extended lambda calculi. However, there are several reasons to also consider other reduction systems than lambda calculus: the following definition for example,

* In-Left (Pair (x,y)) -> x
* In-right (Pair (x,y)) -> y
* Pair (In-left (z), In-right (z)) -> z

cannot be expressed in lambda calculus. The systems we will consider in this talk are Curryfied term rewriting systems.

The talk will start with a short discussion of intersection type assignment for Lambda Calculus, together with its major properties, like

* a strong normalization result,
* a head-normalization result,
* an approximation theorem, together with a filter model,
* principal types.

We will then present Curryfied term rewriting systems together with a notion of intersection type assignment. This notion will be defined using the approach for the lambda calculus, taking the syntactical differences into account. We will discuss what kind of restriction has to be made in order to be able to prove for term rewriting systems similar results (if possible) as above for lambda calculus.
Tuesday 4th July 1995, 14:30
Seminar Room 322
Department of Computer Science