Multiparty session types (MSTs) provide an efficient methodology for specifying and verifying message passing software systems. In the theory of MSTs, a global type specifies the interaction among the roles at the global level. A local specification for each role is generated by projecting from the global type on to the message exchanges it participates in. Whenever a global type can be projected on to each role, the composition of the projections is deadlock free and has exactly the behaviours specified by the global type. The key to the usability of MSTs is the projection operation: a more expressive projection allows more systems to be type-checked but requires a more difficult soundness argument. In this paper, we generalise the standard projection operation in MSTs. This allows us to model and type-check many design patterns in distributed systems, such as load balancing, that are rejected by the standard projection. The key to the new projection is an analysis that tracks causality between messages. Our soundness proof uses novel graph-theoretic techniques from the theory of message-sequence charts. We demonstrate the efficacy of the new projection operation by showing many global types for common patterns that can be projected under our projection but not under the standard projection operation.

翻译：多党会话类型(MSTs)为指定和核实传递的信息的软件系统提供了一种有效的方法。在MSTs理论中,一种全球类型可以指定全球一级角色之间的相互作用。通过从全球类型投射到它所参与的信息交换,可以产生每个角色的本地规格。只要可以预测到每个角色,预测的构成就是一个全球类型,预测的构成是没有僵局的,并且完全具有全球类型所指定的行为。MSTs的可用性关键在于预测操作:一个更直观的预测使得更多的系统能够进行类型检查,但需要一个更困难的正确性论证。在本文中,我们概括了MSTs的标准预测操作。这使我们能够在分布式系统中建模和检查许多设计模式,例如负载平衡,这些模式被标准预测所拒绝。新预测的关键是分析信息之间的因果关系。我们的准确性证据使用了信息序列图表理论中的新图形-理论技术。我们通过展示新的预测操作的功效,显示许多可以在我们预测下预测的通用模式,而不是在标准预测下进行。