Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko
Motohama
Compositional characterization of
lambda -terms using intersection types
Theoret. Comput. Sci., 340(3):459-495, 2005
We show how to characterise compositionally a number of
evaluation properties of lambda-terms using Intersection
Type assignment systems. In particular, we focus on termination
properties, such as strong normalisation, normalisation, head
normalisation, and weak head normalisation. 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 characterisation results are new, to our knowledge, or
else they streamline, strengthen, or generalise earlier results in the
literature.
The completeness parts of the characterisations are proved
uniformly for all the properties, using a set-theoretical semantics
of intersection types over suitable kinds of stable sets. This
technique generalises Krivine's and Mitchell's methods for strong
normalisation to other evaluation properties.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43