The data-parallel programming model is currently the most successful model for programming massively parallel computers. Unfortunately, it is, in its present form, restricted to exploiting flat data parallelism, which is not suitable for some classes of algorithms, e.g. those operating on irregular structures. Recently, some effort has been made to implement nested data-parallel programs efficiently by compiling them into equivalent flat programs using a transformation called flattening. However, previous translations of nested into flat data-parallel programs have proved unwieldy when it comes to inventing and specifying optimizations and verifying the translation. This paper presents a new formalization of the flattening transformation in a calculational style. The formalization is easily verified and provides a good starting point for the development of new optimizations. Some optimizations invented on the basis of this new formalism are described. Furthermore, we present practical evidence obtained by experimenting with an implementation of the transformation.