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.