Type-Based Verification of Message-Passing Parallel Programs

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 paper proposes a decidable dependent type system incorporating abstractions for the various communication operators, a form of primitive recursion, and collective choice. Term types may refer to values in the programming language, including integer, floating point and arrays. The paper further introduces a core programming language for imperative, message-passing, parallel programming, and shows that the language enjoys progress.Under revie