Ale+Dez+Lus:TCS2004 (Article)

Author(s)  Fabio Alessi, Mariangiola DezaniCiancaglini and Stefania Lusin 
Title  « Intersection Types and Domain Operators » 
Journal  Theoret. Comput. Sci. 
Volume  316 
Number  13 
Page(s)  2547 
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 $(\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 minimal fixed point operator. 
@article{Ale+Dez+Lus:TCS2004,
volume = {316},
number = {13},
author = {Alessi, Fabio and DezaniCiancaglini, Mariangiola and Lusin,
Stefania},
fjournal = {Theoretical Compututer Science},
url = {http://www.di.unito.it/~dezani/papers/adl.pdf},
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 = {2547},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)