J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A Calculus for Polymorphic and Polyvariant Flow Types. Journal of Functional Programming 12(3): 183-227, May 2002.
We present λCIL, a typed λ-calculus which serves as the foundation for a typed intermediate language for optimizing compilers for higher-order polymorphic programming languages. The key innovation of λCIL is a novel formulation of intersection and union types and flow labels on both terms and types. These flow types can encode polyvariant control and data flow information within a polymorphically typed program representation. Flow types can guide a compiler in generating customized data representations in a strongly typed setting. Since λCIL enjoys confluence, standardization, and subject reduction properties, it is a valuable tool for reasoning about programs and program transformations.
[PS] [PDF]