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

[Dan Smith]

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