M. Widera and C. Beierle. **An Approach to Checking
the Non-Disjointness of Types in Functional Programming**.
Informatik Berichte 281, FernUniversität Hagen, Januar 2001.

This work motivates a new approach to type
checking functional programs building a bridge between static typing
and soft typing. A type language for this approach can be very
precise; e.g. it may contain large and detailed subtyping
hierarchies. Furthermore, certain requirements on the type language
must be met that differ from usual type definitions. A type language
appropriate for the new typing approach is defined in the first part
of this work.
It turns out that it is a central question for our new type checker
to check whether two types denote sets of values that are
non-disjoint. Since our type language allows for the occurrence of
type variables we are furthermore interested in restricting these
variables as much as possible without reducing the set of common
elements of two types. The second part of this work specifies an
algorithm *CE* that approximates this question and proves the
main properties of *CE*.