[TYPES] Semantics of Intersection Type

[DeLiguoro Ugo]

Hongseok Yang wrote:

 > [The Types Forum, 
http://lists.seas.upenn.edu/mailman/listinfo/types-list]
 >
 >
 > Hi,
 >
 > Would anyone point out the literature on the semantics of 
intersection types?
 > Thanks in advance for the answers.
 >
 > Sincerely,
 > Hongseok
 >

(I probaby sent my reply just to the sender, instead of the list; I 
profit of this mistake to add something to the previous reply: apologies.)

Semantics of intersection types gradually emerged from the study of 
models of the untyped lambda-calculus, and from the completeness theorem 
of intersection type assignment system in the JSL paper (see the message 
by van Bakel for the precise reference): "A filter lambda model and the 
completeness of type assignment" by Barendregt, Coppo and Dezany.
After some years it came out that it is a special case of Stone duality 
of inf semilattices and domains, as pointed out firstly by Abramsky in 
his APAL paper "Domains in Logical Form": as such intersection types can 
be seen as syntax to decsribe compact points in a domain, which is a 
topological lambda-model. A very elementary introduction to the topic 
can be found in sections 10-12 of M. Dezani-Ciancaglini, E. Giovannetti, 
and U. de' Liguoro. Intersection types, lambda-models and Böhm trees. In 
MSJ-Memoir Vol. 2 ``Theories of Types and Proofs'', volume 2, pages 
45-97. Mathematical Society of Japan, 1998. See also the references 
there, as well as the subsequent papers on the subject by Dezani and 
others tha can be found at www.di.unito.it/~dezani. A concise 
presentation of D_\infty via intersection types can be found in chapter 
3 of R. M. Amadio, P.-L. Curien book "Domains and Lambda-Calculi", 
Cambridge Un. Press 1998. A gentle introduction to Stone duality and 
computer science, beside Abramsky's paper and chapter 10 of 
Amadio-Curien book, is S. Vickers book "Topology via Logic" Cambridge 
Un. Press. 1989.

All the best, Ugo de' Liguoro