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

[Benjamin Pierce]

There's been a huge amount of work in this area since the papers you  
mentioned.  Joshua Dunfield's recent (CMU) PhD thesis has a pretty  
comprehensive bibliography.  Also check out the CDuce web page.

Best,

    - Benjamin


On Apr 9, 2008, at 11:15 AM, Dan Smith wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Benjamin Pierce's PhD work involved a calculus combining System F,
> intersection types, and bounded quantification (Programming With
> Intersection Types and Bounded Polymorphism, 1991).  His earlier work
> aspired to including union types in this calculus as well, but that
> was apparently dropped (Programming with Intersection Types, Union
> Types, and Polymorphism, 1991).
>
> What is the best place to find a similar calculus that includes union
> types?  In particular, I'm looking for a similar formal treatment of
> subtyping that includes the following rules ("&" is intersection; "|"
> is union):
>
> S->T1 & S->T2 <: S->(T1 & T2)
>
> S1->T & S2->T <: (S1 | S2)->T
>
> Any help would be appreciated.
>
> --Dan