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

 Ale+Dez+Lus:TCS-2004 (Article) Author(s) Fabio Alessi, Mariangiola Dezani-Ciancaglini and Stefania Lusin Title « Intersection Types and Domain Operators » Journal Theoret. Comput. Sci. Volume 316 Number 1--3 Page(s) 25--47 Year 2004 URL http://www.di.unito.it/~dezani/papers/adl.pdf
 Abstract We use intersection types as a tool for obtaining $\lambda$-models. Relying on the notion of easy intersection type theory we successfully build a $\lambda$-model in which the interpretation of an arbitrary simple easy term is any filter which can be described by a continuous predicate. This allows us to prove two results. The first gives a proof of consistency of the $\lambda$-theory where the $\lambda$-term $\left(\lambda x.xx\right)\left(\lambda x.xx\right)$ is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of $\lambda$-theories. The second result is that for any simple easy term there is a $\lambda$-model where the interpretation of the term is the minimal fixed point operator.

 BibTeX code

@article{Ale+Dez+Lus:TCS-2004,
volume = {316},
number = {1--3},
author = {Alessi, Fabio and Dezani-Ciancaglini, Mariangiola and Lusin,
Stefania},
fjournal = {Theoretical Compututer Science},
title = {{Intersection Types and Domain Operators}},
abstract = {We use intersection types as a tool for obtaining
$\lambda$-models. Relying on the notion of {\em easy intersection
type theory} we successfully build a $\lambda$-model in which the
interpretation of an arbitrary simple easy term is any filter
which can be described by a continuous predicate. This allows us
to prove two results. The first gives a proof of consistency of
the $\lambda$-theory where the $\lambda$-term $(\lambda x.xx)(\lambda x.xx)$ is forced to behave as the join operator.
This result has interesting consequences on the algebraic
structure of the lattice of $\lambda$-theories. The second result
is that for any simple easy term there is a $\lambda$-model where
the interpretation of the term is the {\em minimal} fixed point
operator. },
year = {2004},
journal = {Theoret. Comput. Sci.},
pages = {25--47},
}

 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) 