We presentParTypes, a type discipline for parallel programs. The model we have in mind comprises a fixed number of processes running in parallel and communicating via collective operations or point-to-point synchronous message exchanges. A type describes a protocol to be followed by each processes in a given program. We present the type theory, a core imperative programming language and its operational semantics, and prove that type checking is decidable (up to decidability of semantic entailment) and that well-typed programs do not deadlock and always terminate. The article is accompanied by a large number of examples drawn from the literature on parallel programming.

@article{paperbot1601,
  title = {A Type Discipline for Message Passing Parallel Programs},
  author = {Vasco T. Vasconcelos and Francisco Martins and Hugo-Andrés López and Nobuko Yoshida},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {44},
  number = {4},
  year = {2022},
  doi = {10.1145/3552519}
}