Subtyping Union Types

Subtyping can be fairly complex for union types, due to interactions with other types, such as function types. Furthermore, these interactions turn out to depend on the calculus considered: for instance, a call-by-value calculus and a call-by-name calculus will have different possible subtyping rules. In order to abstract ourselves away from this dependence, we consider a fairly large class of calculi. This allows us to find a subtyping relation which is both robust (it is sound for all calculi) and precise (it is complete with respect to the class of calculi)