alesdezahons04 (In proceedings)
|
Author(s) | Fabio Alessi, Mariangiola Dezani-Ciancaglini 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) | 3-25 |
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 set-theoretic intersection operation and arrow type constructor as set-theoretic function space constructor. In this paper we study the relation between natural intersection type preorders and natural -structures, i.e. -algebraic lattices with Galois connections given by and . We prove on one hand that natural intersection type preorders induces natural -structures, on the other hand that natural -structures admits presentations through intersection type preorders. Moreover we give a concise presentations of classical models of untyped -calculus through suitable natural intersection type preorders and prove that filter models induced by them are isomorphic to . |
@inproceedings{alesdezahons04,
author = {Alessi, Fabio and Dezani-Ciancaglini, 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
set-theoretic intersection operation and arrow type constructor as
set-theoretic 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 = {3-25},
year = {2004},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)