alesdezahons04 (In proceedings)

Author(s)  Fabio Alessi, Mariangiola DezaniCiancaglini and Furio Honsell 
Title  « Inverse Limit Models as Filter Models » 
In  HOR'04 
Editor(s)  Delia Kesner, Femke van Raamsdonk and Joe Wells 
Page(s)  325 
Year  2004 
Publisher  RWTH Aachen 
Address  Aachen 
URL  http://www.di.unito.it/~dezani/papers/adh.pdf 
Abstract 
Natural intersection type preorders are the type structures which agree with the plain intuition of intersection type constructor as settheoretic intersection operation and arrow type constructor as settheoretic function space constructor. In this paper we study the relation between natural intersection type preorders and natural $\lambda $structures, i.e. $\omega $algebraic lattices $D$ with Galois connections given by $F:D\to \; [D\to \; D]$ and $G:[D\to \; D]\to \; D$. We prove on one hand that natural intersection type preorders induces natural $\lambda $structures, on the other hand that natural $\lambda $structures admits presentations through intersection type preorders. Moreover we give a concise presentations of classical $D$_{∞} models of untyped $\lambda $calculus through suitable natural intersection type preorders and prove that filter models induced by them are isomorphic to $D$_{∞}. 
@inproceedings{alesdezahons04,
author = {Alessi, Fabio and DezaniCiancaglini, Mariangiola and Honsell,
Furio},
booktitle = {HOR'04},
editor = {Delia Kesner and Femke van Raamsdonk and Joe Wells},
url = {http://www.di.unito.it/~dezani/papers/adh.pdf},
address = {Aachen},
title = {{Inverse Limit Models as Filter Models}},
abstract = {Natural intersection type preorders are the type structures which
agree with the plain intuition of intersection type constructor as
settheoretic intersection operation and arrow type constructor as
settheoretic function space constructor. In this paper we study
the relation between natural intersection type preorders and
natural $\lambda$structures, i.e. $\omega$algebraic lattices $D$
with Galois connections given by $F:D\rightarrow [D\rightarrow D]$
and $G:[D\rightarrow D]\rightarrow D$. We prove on one hand that
natural intersection type preorders induces natural
$\lambda$structures, on the other hand that natural
$\lambda$structures admits presentations through intersection
type preorders. Moreover we give a concise presentations of
classical $D_\infty$ models of untyped $\lambda$calculus through
suitable natural intersection type preorders and prove that filter
models induced by them are isomorphic to $D_\infty$.},
publisher = {RWTH Aachen},
pages = {325},
year = {2004},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)