Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia
Likavec
Behavioural inverse limit
lambda-models
Theoret. Comput. Sci., 316(1-3):49-74, 2004
We construct two inverse limit lambda-models
which completely characterise sets of terms with
similar computational behaviours: the sets of
normalising, head normalising, weak head normalising
lambda-terms, those corresponding to the
persistent versions of these notions, and the sets
of closable, closable normalising, and closable head
normalising lambda-terms. More precisely, for
each of these sets of terms there is a corresponding
element in at least one of the two models such that
a term belongs to the set if and only if its
interpretation (in a suitable environment) is
greater than or equal to that element. We use the
finitary logical description of the models, obtained
by defining suitable intersection type assignment
systems, to prove this.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43