We present a type-based approach to the verification of the communication structure of parallel programs. We model parallel imperative programs where a fixed number of processes, each equipped with its local memory, communicates via a rich diversity of primitives, including point-to-point messages, broadcast, reduce, and array scatter and gather. The theory includes a decidable dependent type system incorporating abstractions for the various communication operators, a form of primitive recursion, and collective choice. We further introduce a core programming language for imperative, message-passing, parallel programming, and show that the language enjoys progress. Joint work with Francisco Martins, Eduardo R.B. Marques, Hugo A. López, César Santos and Nobuko Yoshida.