Typed Intermediate Languages for Shape Analysis

We introduce S2, a typed intermediate language for vectors, based on a 2-level type-theory, which distinguishes between compile-time and run-time. The paper shows how S2 can be used to extract useful information from programs written in the Nested Sequence Calculus N SC, an idealized high-level parallel calculus for nested sequences. We study two translations from N SC to S2. The most interesting shows that shape analysis (in the sense of Jay) can be handled at compile-time