M. Dezani-Ciancaglini and S. Ghilezan
Two behavioural lambda models
In Types'02, volume 2246 of LNCS, pages 127-147
Springer-Verlag, 2003
We build two inverse limit lambda models which characterize
completely sets of terms having similar computational
behaviour. More precisely for each one 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. This is proved by using the finitary logical
description of the models obtained by defining suitable
intersection type assignment systems.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43