A calculus with polymorphic and polyvariant flow types

JB Wells, A Dimock, R Muller, F Turbak - Journal of Functional …, 2002 - cambridge.org
JB Wells, A Dimock, R Muller, F Turbak
Journal of Functional Programming, 2002cambridge.org
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 …
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.
Cambridge University Press