Vasconcelos, Vasco T.Martins, FranciscoMarques, Eduardo R. B.López, Hugo A.Santos, CésarYoshida, Nobuko2014-10-292014-11-142014-10-292014-11-142014-10-29http://hdl.handle.net/10451/14194http://repositorio.ul.pt/handle/10455/6902We 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.engsession typesmessage passingtype-based verificationparallel programsreport