Dez+Ghi+Lik:TCS2004 (Article)

Author(s)  Mariangiola DezaniCiancaglini, Silvia Ghilezan and Silvia Likavec 
Title  « Behavioural Inverse Limit Models » 
Journal  Theoret. Comput. Sci. 
Volume  316 
Number  13 
Page(s)  4974 
Year  2004 
URL  http://www.di.unito.it/~dezani/papers/dgl.pdf 
Abstract 
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. 
@article{Dez+Ghi+Lik:TCS2004,
volume = {316},
number = {13},
author = {DezaniCiancaglini, Mariangiola and Ghilezan, Silvia and Likavec,
Silvia},
fjournal = {Theoretical Compututer Science},
url = {http://www.di.unito.it/~dezani/papers/dgl.pdf},
title = {{Behavioural Inverse Limit Models}},
abstract = {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.},
year = {2004},
journal = {Theoret. Comput. Sci.},
pages = {4974},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)