一句话：提出 ParTypes 类型规约，为消息传递并行程序规定协议，并保证类型检查可判定、良类型程序无死锁且终止。
论文提出 ParTypes，一种用于消息传递并行程序的类型规约。其模型由固定数量的并行进程组成，进程通过集合操作或点对点同步消息交换进行通信；类型刻画每个进程在程序中必须遵循的协议。作者给出了类型理论、一个核心命令式语言及其操作语义，并在此基础上证明类型检查是可判定的（在语义蕴含可判定的前提下），同时证明良类型程序不会死锁且总能终止。文中还用大量来自并行编程文献的示例说明该类型规约的表达能力与用法。
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}
}