[TYPES] Formal treatment of intersection/union/arrow subtyping?

[gc@pps.jussieu.fr]

Dan Smith wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Thank you all for your useful pointers.
> 
> In skimming a number of papers related to these references, I have yet  
> to come upon the ideal presentation I'm looking for.  I would love to  
> see a paper that:
> 

You can probably find a good match (the calculus aside) in a paper by 
Mariangiola Dezani et al "The relevance of semantic subtyping".

http://www.di.unito.it/~dezani/papers/itrs02.pdf

Look in particular in Section 3. The paper is more logic-oriented than 
functional programming oriented howver it will also give you an idea on the 
relation about what you are looking for and a streamlined version of semantic 
subtyping without negation types.

> - Extends lambda-sub (the simply-typed lambda-calculus with subtyping)  
> with intersection and union types.

Church style or Curry style? It is quite likely to make a difference.


---Beppe---