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

 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 $\lambda$-structures, i.e. $\omega$-algebraic lattices $D$ with Galois connections given by $F:D\to \left[D\to D\right]$ and $G:\left[D\to D\right]\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$∞.

 BibTeX code

@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},
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},
}

 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)