# [TYPES] Semantics of Intersection Type

DeLiguoro Ugo deligu at di.unito.it
Wed Nov 30 07:38:48 EST 2005

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?
>
> 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
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