[TYPES] Semantics of Intersection Type

[Gerard Boudol]

Hongseok Yang wrote:

>[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>Would anyone point out the literature on the semantics of 
>intersection types? 
>  
>

as far as I can see, the answers you got on the TYPES list all interpret 
your question as "what is the use of intersection types in semantics?" 
And the obvious answer is that they provide, by means of the "filter 
models", a concrete presentation of some well-know domains for 
interpreting lambda-calculi, where the types determine the compact 
elements (I myself wrote a paper on this topic, published in Information 
and Computation, Vol. 108, No. 1, 1994).

But one could understand your question in another way, namely : "what 
can be a semantical interpretation of (intersection) types". Then an 
obvious answer is: a set of expressions of some calculus (the 
"realizability" interpretation of types), or more generally a set of 
elements in some model of the calculus. Generalizing this to predicates 
indexed by types, one gets the notion of a "logical relation".  Some 
good references from this point of view are Krivine's book on 
"Lambda-Calculus, Types and Models" (Ellis Horwood, 1993), Mitchell's  
"Foundations for Programming Languages" (MIT Press, 1996), and Amadio 
and Curien's "Domains and Lambda-Calculi" (Cambridge University Press, 
1998), which also contains a chapter on filter models.

Interestingly, combining these two viewpoints on types is most fruitful, 
in establishing for instance full abstraction results, like the 
classical one by Wadsworth regarding Scott's interpretation of the pure 
lambda-calculus. A nice presentation of this is in Ronchi's lectures 
notes on "Basic Lambda Calculus" (1998? I don't know whether these notes 
have been published).

Best regards,

Gérard Boudol