Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are 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 »
InHOR'04
Editor(s) Delia Kesner, Femke van Raamsdonk and Joe Wells
Page(s)3-25
Year2004
PublisherRWTH Aachen
AddressAachen
URLhttp://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 D with Galois connections given by F:D→ [D→ D] and G:[D→ D]→ D. 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 D models of untyped λ-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},
  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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are 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)

Valid HTML 4.01!