Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

 Dez+Ghi+Lik:TCS-2004 (Article) Author(s) Mariangiola Dezani-Ciancaglini, Silvia Ghilezan and Silvia Likavec Title « Behavioural Inverse Limit Models » Journal Theoret. Comput. Sci. Volume 316 Number 1--3 Page(s) 49--74 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.

 BibTeX code

@article{Dez+Ghi+Lik:TCS-2004,
volume = {316},
number = {1--3},
author = {Dezani-Ciancaglini, 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:
$\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 = {49--74},
}

 Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)