Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Furio
Honsell
Inverse limit models as filter models
In Delia Kesner, Femke van Raamsdonk, and J. B. Wells, editors,
HOR '04, pages 3-25, Aachen, 2004 RWTH Aachen
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 with Galois connections given by
F:-> [-> ] and
G:[-> ]-> . 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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43