异步混合选择在多党会话类型中的应用

异步多方会话类型可实现性是可判定的——来自消息序列图的经验教训

Asynchronous Multiparty Session Type Implementability is Decidable -- Lessons Learned from Message Sequence Charts

该研究解决了具有发送方驱动选择的异步多方会话类型可实现性的可判定性开放问题，通过推广高级消息序列图的结论给出肯定答案，同时研究了相关技术适配并证明了一类推广的可实现性问题不可判定。

从本地会话类型合成编排（扩展版）

Synthesising Choreographies from Local Session Types (extended version)

设计和分析多方分布式交互可以通过全局视图（例如基于编排的方法）或通过组成可用的计算实体（例如服务编排）来实现。本文提出了一种类型化系统，它允许在某些条件下，从一组描述端点行为（即本地类型）的本地会话类型中合成编排（即多方全局类型）。

设计具有崩溃停止故障的异步多方协议

Designing Asynchronous Multiparty Protocols with Crash-Stop Failures

针对分布式系统故障，提出Teatrino工具链，基于崩溃停止语义的异步多方会话类型，扩展Scribble和Effpi生成协议一致的Scala代码，保证无死锁、一致性和活性。

多方对称和类型

Multiparty Symmetric Sum Types

本文介绍了一种新的基于对称和类型的多方会话类型的理论，我们可以类型的非确定性的编排选择行为。虽然会话类型中的原始分支类型可以表示由单个参与者做出并被其他参与者接受的决定会话如何进行的选择，但对称和类型表示由会话的所有参与者之间的协议做出的选择。这种行为可以在许多实际系统中找到，包括用于临床实践指南（CPG）的医疗保健系统中的协作工作流。使用对称和的过程可以嵌入到使用导体过程的原始分支类型中。我们表明，这种类型驱动的嵌入保留类型，满足语义的健全性和完整性，并满足编码标准适应类型设置。该理论导致了一个有效的实现的原型工具，自动翻译的原始CPG规范从一个表示称为过程矩阵的对称和类型，类型检查程序，并执行它们。

Quorums Quicken加密：高效的异步安全多方计算

Quorums Quicken Queries: Efficient Asynchronous Secure Multiparty Computation

我们描述了一个异步算法来解决安全多方计算（MPC）在n个球员，当严格小于1/8的分数的球员是由一个静态对手控制。对于域上的任何函数f，可以由具有m个门的电路计算，我们的算法要求每个参与者发送多个域元素，并执行O（m/n + \sqrt{n}）的计算量。这比传统算法有了显著的改进，传统算法需要每个玩家发送大量消息并执行Ω（nm）的计算。此外，我们定义了阈值计数问题，并提出了一个分布式算法来解决它在异步通信模型。我们的算法是负载平衡的，计算，通信和延迟的O（log n）的复杂性，并可能是独立的利益，其他应用程序的负载均衡的目标。

CoMPSeT：一种用于比较多方会话类型的框架

CoMPSeT: A Framework for Comparing Multiparty Session Types

针对现有多方会话类型（MPST）变体特性各异、难以对比的问题，研究人员提出开源工具框架CoMPSeT，可组合不同MPST特性、动画演示并比较示例语义，支持浏览器直接运行，助力MPST研究与教学。

带全局跳出循环的容错多方会话类型

Fault-Tolerant Multiparty Session Types with Global Escape Loops

该研究扩展了带故障模式的容错多方会话类型FTMPST，新增无需全局协调、带非阻塞退出消息的全局跳出容错循环结构，并通过旋转协调器算法变体验证了方法的可行性，为容错分布式算法的属性验证提供支持。

Statically Verified Refinements for Multiparty Protocols

With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom. While originally MPST focus on the communication aspects, and employ a simple typing system for communication payloads, communication protocols in the real world usually contain constraints on the payload. We introduce refined multiparty session types (RMPST), an extension of MPST, that express data d…

用于多方对话的定时监听

Timed Runtime Monitoring for Multiparty Conversations

提出了一个实时分布式系统中协议的动态验证框架。该框架基于Scribble，这是一种与我们的工业合作伙伴共同开发的工具链，用于设计和验证基于多方会话类型的编排。从最近的工作，多方会话类型的实时交互，我们扩展涂鸦时钟，重置，时钟谓词约束的时间，互动应该发生。我们提出了一个定时的Python API来编程Scribble规范的分布式实现。动态验证框架确保了使用我们的定时API编写的应用程序的安全执行：我们已经实现了专用的运行时监视器，可以检查每个交互是否在相应的Scribble规范的正确时间发生。我们的实施和它的实用性的性能进行了分析，通过基准。

异步二元会话的公平终止

Fair Termination of Asynchronous Binary Sessions

本文提出基于线性逻辑的异步会话类型理论，利用新颖的公平异步子类型关系保证良类型进程在公平性假设下公平终止，实现无饥饿与无孤儿消息。

在HML中嵌入会话类型

Embedding Session Types in HML

最近的工作是用逻辑注释增强多方会话类型，从而能够有效地验证以下属性：（1）会话的结构，（2）消息的种类，以及（3）交换的实际值。在[3]中，我们扩展了这项工作，以实现多个跨会话交互的相互影响的规范和验证。在这里，我们给出了一个声音和完整的嵌入到Hennessy-Milner逻辑，以证明[3]中的方法的表达能力，并为它提供一个逻辑背景，使我们能够将其与类似的方法进行比较。

Parallel Monitors for Self-adaptive Sessions

The paper presents a data-driven model of self-adaptivity for multiparty sessions. System choreography is prescribed by a global type. Participants are incarnated by processes associated with monitors, which control their behaviour. Each participant can access and modify a set of global data, which are able to trigger adaptations in the presence of critical changes of values. The use of the parallel composition for building global types, monitors and processes enables a significant degree of flexibility: an adaptation step can dynamically reconfigure a set of participants only, without alterin…

作为合同协议的编舞合成

Choreography Synthesis as Contract Agreement

我们提出了一个分布式系统的正式模型，每个参与者都将其要求和义务作为行为合同，当一组合同允许合成编排时，多方会话开始。我们的框架是基于CO2演算面向合同的计算，并借用会话类型的文献的概念和结果。它支持参与者的数量没有事先确定的会话，并保持CO2的能力，以排除那些在运行时没有履行合同的参与者。我们表明，由于参与者的诚实，我们在CO2中取得了进展和会话保真度-即，他们总是遵守合同的能力。

参数化并发多方会话类型

Parameterized Concurrent Multi-Party Session Types

会话类型已被提议作为静态验证通信协议的实现的手段。虽然以前的工作已经成功地验证了某些类的协议，它不能很好地处理参数化，多演员的情况下，固有的安全性。例如，滑动窗口协议在先前提出的会话类型系统中是不可表达的。本文介绍了System-A，一种新的类型化语言，它克服了许多以前的工作的表现力的限制。System-A显式地支持并行和并行，以及多种形式的参数化。我们定义了系统A，并展示了它如何可以用于一个大类的异步通信协议的静态验证。