Abstract of Paper

Compositional Characterizations of $\lambda$-terms Using Intersection Types
by M.Dezani-Ciancaglini, F.Honsell and Y.Motohama

Abstract:

We show how to characterize compositionally a number of evaluation
properties of $\lambda$-terms using Intersection Type assignment systems. In
particular, we focus on termination properties, such as strong
normalization, normalization, head normalization, and weak head
normalization. We consider also the persistent versions of such notions. By
way of example, we consider also another evaluation property, unrelated to
termination, namely reducibility to a closed term.
 
Many of these characterization results are new, to our knowledge, or else
they streamline, strengthen, or generalize earlier results in the
literature.
 
The completeness parts of the characterizations are proved uniformly, for
all the properties, using a set-theoretical semantics of intersection types
over suitable kinds of stable sets. This technique generalizes Krivine's and
Mitchell's methods for strong normalization to other evaluation properties
besides.