一句话：提出函数式多参与方会话类型语言MPGV，支持一等端点并保持无死锁性，结果已在Coq中机器验证。
会话类型已被集成到函数式语言中，使通道端点成为一等值，可存入数据结构、被闭包捕获并沿通道传递。GV 系列因与线性逻辑的 Curry-Howard 对应而同时保证会话保真性与无死锁性，但现有版本仅支持二元会话，一次会话只能有两个参与者。本文提出 MPGV，一种带多参与方会话类型的函数式语言，允许多个参与者并发交互。MPGV 在会话交错与委托下仍保持 GV 的强保证，包括无死锁性；其新颖的重定向构造支持一等端点的模块化编程。作者给出从二元会话类型到 MPGV 的类型保持翻译，证明 MPGV 严格比二元 GV 更一般，并用 Coq 机器化所有结果。
Session types have recently been integrated with functional languages, bringing message-passing concurrency to functional programming. Channel endpoints then become first-class and can be stored in data structures, captured in closures, and sent along channels. Representatives of the GV (Wadler's "Good Variation") session type family are of particular appeal because they not only assert session fidelity but also deadlock freedom, inspired by a Curry-Howard correspondence to linear logic. A restriction of current versions of GV, however, is the focus on binary sessions, limiting concurrent interactions within a session to two participants. This paper introduces Multiparty GV (MPGV), a functional language with multiparty session types, allowing concurrent interactions among several participants. MPGV upholds the strong guarantees of its ancestor GV, including deadlock freedom, despite session interleaving and delegation. MPGV has a novel redirecting construct for modular programming with first-class endpoints, thanks to which we give a type-preserving translation from binary session types to MPGV to show that MPGV is strictly more general than binary GV. All results in this paper have been mechanized using the Coq proof assistant.
@article{paperbot1504,
title = {Multiparty GV: functional multiparty session types with certified deadlock freedom},
author = {Jules Jacobs and Stephanie Balzer and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547638}
}