d Abstract) James Riely1 and Jan Prins2 1 DePaul University 2 University of North Carolina at Chapel Hill Abstract. Flattening is a program transformation that eliminates nested parallel constructs, introducing flat parallel (vector) operations in their place. We define a sufficient syntactic condition for the correctness of flattening, providing a static approximation of Blelloch's "containment". This is achieved using a typing system that tracks the control flow of programs. Using a weak improvement preorder, we then show that the flattening transformations are intensionally correct for all well-typed programs.