Modular Multiparty Sessions with Mixed Choice
本文提出一种面向多方会话的类型指派方法，将混合选择限制在松散耦合模块内部使用，从而在提升表达能力的同时保证主体归约、会话保真性和无锁性。
2025-08-19 cs.LO
Precise Subtyping for Asynchronous Multiparty Sessions
本文提出了第一个形式化的精确子类型关系的异步多方会话。我们证明了我们的子类型关系是合理的（即，保证安全的进程替换），并且也是完全的：关系的任何扩展都是不可靠的。为了实现我们的结果，我们开发了一种新的会话分解技术，从完整的会话类型（包括内部/外部选择）到单个输入/输出会话树（没有选择）。以前的工作研究了二进制会话（只有两个参与者）或多方会话（任何数量的参与者）和同步交互的精确子类型。在这里，我们涵盖了多方会话与异步交互，消息通过FIFO队列（如TCP/IP协议）传输，并证明我们的子类型是操作和外延精确。在异步多方设置中，找到精确的子类型关系是一项非常复杂的任务：这是因为，在某些条件下，参与者可以通过提前发送一些消息或稍后接收一些消息来排列其输入和输出的顺序，而不会导致错误;精确的子类型关系必须捕获所有这些有效的排列-因此，其形式化，推理和证明变得具有挑战性。我们的会话分解技术克服了这种复杂性，表示子类型的关系作为一个组成的细化之间的关系的单一输入/输出树，并提供了一个简单的推理原则，异步消息优化。
2020-10-26 cs.LO
Separation and Encodability in Mixed Choice Multiparty Sessions (Technical Report)
本文为混合选择同步多方会话演算提出通用类型系统并证明其安全性，进而通过可编码性与分离性分析比较九个演算的表达能力，证明MCMP严格强于经典多方会话。
2024-06-07 cs.LO
FTMPST: Fault-Tolerant Multiparty Session Types
本文扩展多方会话类型以集成容错机制，应对不可靠通信和进程崩溃等系统故障，并通过故障模式增强进程语义，成功应用于分析Chandra和Toueg的旋转协调器算法变体。
2023-11-24 cs.LO
Parameterised Multiparty Session Types
对于许多应用级分布式协议和并行算法，参与者的集合、消息的数量或交互结构仅在运行时才知道。本文提出了一个多方会话的依赖类型论，它可以静态地保证类型安全的，无死锁的多方进程之间的互动，其规格由索引参数化。我们使用哥德尔系统T中的原始递归运算符来表达广泛的通信模式，同时保持类型检查的可判定性。为了对单个分布式进程进行类型化，将参数化的全局类型投影到表示所有可能的端点类型的类的通用生成器上。我们证明了终止的类型检查算法在整个系统与多方会话类型和递归类型。我们说明了我们的类型论通过非平凡的编程和验证的例子，从并行算法和Web服务用例。
2012-10-10 cs.LO
A Typeful Characterization of Multiparty Structured Conversations Based on Binary Sessions
将分布式系统的全局通信行为的规范与其每个节点/对等体的本地通信行为的规范（例如，检查前者在某些安全和/或活性条件下是否可由后者实现）是在许多相关场景中解决的具有挑战性的问题。在网络化软件服务的上下文中，广泛使用的基于程序设计语言的方法依赖于由会话类型或行为契约定义的全局规范。然后可以使用静态类型检查来确保组件遵循规定的交互协议。在会话类型的情况下，发展主要是在完全不同的类型论的二元（两方）或多方（n方）协议。不幸的是，多方和二进制协议的分析技术之间的精确关系还有待理解。在这项工作中，我们弥合这一以前开放的差距在原则上的方式：我们表明，多方协议的分析也可以在一个更简单的类型论的二进制协议，确保协议的保真度和死锁自由。我们提出的特征定理，提供了新的见解之间的关系，但非常不同的动机，会话类型系统-一个基于线性逻辑，其他基于自动机理论-并建议有用的基于类型的验证技术，多方系统依赖于减少到二进制的情况。
2014-07-16 cs.LO
Taming Concurrency for Verification Using Multiparty Session Types (Technical Report)
分布式系统中并发通信进程所带来的额外复杂性使得此类系统的验证成为一个非常困难的问题。多方会话类型被开发用于管理分布式系统中的通信和并发。因此，它们提供了一种有效的验证方法w.r.t.关于通信和并发的属性，如通信安全或进度。但是，它们不支持需要考虑具体运行或变量具体值的特性分析。我们sequentialise良好的类型系统的进程的结构，其全球类型的指导下，以获得其相互作用的抽象。如果没有交互，系统中的并发性将减少到顺序和完全独立的并行组合。在这样的抽象中，对诸如例如基于数据的终止之类的属性的验证变得更加有效，这些属性不被多方会话类型覆盖，而是依赖于变量的具体运行或值。
2019-08-18 cs.LO
On Asynchronous Multiparty Session Types for Federated Learning
Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；Technical University of Denmark（丹麦技术大学）；University of Oxford（牛津大学）
本文改进了会话类型理论，以支持建模和验证实现联邦学习协议的过程。通过引入面向多个参与者的输入/输出操作，增强了灵活性并允许安全的过程替换。
2026-03-26 cs.LO
Multiparty Sessions based on Proof Nets
我们解释线性逻辑证明网的术语语言的基础上Solos演算。该系统包括一个同步机制，通过逻辑的保守扩展获得，能够定义非确定性行为和多方会话。
2014-06-13 cs.LO cs.PL
Formally Verified Liveness with Multiparty Session Types in Rocq
University of Edinburgh（爱丁堡大学）；University of Oxford（牛津大学）；School of Computer Science and Engineering, University of New South Wales（新南威尔士大学计算机科学与工程学）
本文在Rocq证明助手中首次机械化证明了同步多方会话类型的活性，利用共归纳树和子类型关系建立局部类型与全局类型的操作对应，从而保证会话的安全性和活性。
2026-05-22 cs.LO
Fair Termination of Multiparty Sessions
存在一个广泛的多方会话家族，其中一个会话参与者的进展不是无条件的，而是取决于其他参与者执行的选择。这些会话不属于当前可用的保证进度的会话类型系统的范围。在这项工作中，我们提出了第一个类型系统，确保良好类型的多方会话，包括那些表现出上述依赖关系，公平地终止。公平终止是在公平假设下的终止，该假设忽略了那些被认为不公平因而不现实的互动。公平终止与会话内确保的通常的安全属性相结合，不仅本身是期望的，而且它需要进步并实现静态分析的组合形式，使得公平终止会话的良好类型的组合导致公平终止程序。
2022-05-18 cs.LO cs.PL
A Logical Interpretation of Asynchronous Multiparty Compatibility
本文在命题即类型框架下将多方兼容性的相干性条件推广为转发器，并证明转发器完全刻画所有类型良好的多方兼容进程。
2023-05-25 cs.LO
Imprecise Probability for Multiparty Session Types in Process Algebra
在本文中，我们引入不精确的概率会话类型。更确切地说，我们使用的概率过程演算，其中考虑了非确定性的外部选择和概率性的内部选择。我们提出的概率多方会话类型能够编纂的通信结构，通过使用一些不精确的概率方面的下限和上限的概率。我们证明了这个新的概率分型系统是健全的，以及其他几个结果处理经典和概率性质。该方法说明了一个简单的例子，启发调查民意调查。
2020-02-19 cs.LO math.PR
Secure Multiparty Sessions with Topics
多方会话演算最近已经配备了安全要求，以保证属性，如访问控制和泄漏自由。然而，拟议的安全要求在某些情况下似乎限制性过强。特别是，一方在收到秘密信息后，不允许传播任何种类的公共信息。如果这两条信息完全不相关，这似乎是不合理的。本文的目的是克服这一限制，方法是为简单的多方会话演算设计一个类型规程，该规程根据消息的主题对消息进行分类，并允许对独立主题的消息进行不受限制的排序。
2016-06-20 cs.DC cs.LO
Propositions in Linear Multirole Logic as Multiparty Session Types
我们确定多角色逻辑作为一种新形式的逻辑和形式化线性多角色逻辑（LMRL）作为一个自然的推广经典线性逻辑（CLL）。在为LMRL建立的各种元性质中，我们得到了一个称为多割消去的元性质，即三个（或更多）序列之间的每一个割（作为两个序列之间的割的推广）都可以消去，从而推广了Gentzen关于割消去的著名结果.我们还提出了一个变体的$π$ -演算的多方会话，证明了一个紧密的对应关系，在这个变体的过程中的通信和多割消除LMRL，从而扩展了Caires和Pfenning（2010）和Wadler（2012）的一些最近的结果，以及其他类似的工作。
2016-11-27 cs.LO cs.PL
Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report)
会话类型支持通信系统的规范和验证。然而，他们的理论通常假设过程永远不会失败。为了解决这个问题，我们提出了一个广义多方会话类型（MPST）理论与崩溃停止故障，其中进程可以崩溃任意。我们的新理论验证了更多的协议和过程w.r.t.以前的工作。我们将最小的语法变化应用于标准会话π-演算和类型：我们对崩溃及其处理进行语义建模，并在行为安全属性上使用广义MPST类型系统参数。我们涵盖了完全可靠和完全不可靠的会话之间的频谱，通过可选的可靠性假设，并证明了类型安全性和协议一致性的崩溃停止故障的存在。引入崩溃停止失败会产生重要的后果：编写处理所有崩溃场景的正确进程可能很困难。然而，我们的广义MPST理论允许我们驯服这种复杂性，通过模型检验，以验证多方会话是否满足所需的行为属性，例如死锁自由或活性，即使在崩溃的存在。我们使用mCRL 2模型检查器实现我们的方法，并从文献中扩展的例子进行评估。
2023-02-21 cs.LO cs.PL
Mixed Choice Multiparty Session Types, Precisely
University of Oxford（牛津大学）
本文针对含会话委托等特性的混合选择多方会话类型，证明其子类型关系的精确性，开发通用类型系统并实现相关检查算法，经案例研究验证其有效性。
2026-08-12 cs.LO cs.PL
Globally Governed Session Semantics
本文提出了一种基于多方会话类型的互模拟理论，其中编排规范管理会话类型进程及其观察者的行为。互模拟的定义与观察者与所观察到的进程合作，以形成完整的全局会话场景，并可用于证明全局协调线程和进程的优化的正确性。诱导互模拟比标准会话互模拟严格地更细粒度。只有当存在两个以上的交错多方会话时，受控制的互模拟和标准互模拟之间的差异才会出现。这个独特的功能使得能够在大规模分布式系统中推理真实场景，其中多个编排会话需要交错。通过关于受支配的基于约简的同余的可靠性和完备性，证明了受支配的双相似性的组合性。最后，在一个大规模网络基础架构的实际应用中，通过一个多会话控制下的线程转换演示了该方法的使用。
2015-03-01 cs.LO
Compositional Interface Refinement Through Subtyping in Probabilistic Session Types
本文提出概率混合选择多方会话π演算及其灵活子类型系统，允许用多个通道细化单个接口，并证明主体归约、无错误性和无死锁性，从而支持概率分布式通信的组合式验证与逐步细化。
2025-09-12 cs.LO
Fault-Tolerant Multiparty Session Types with Global Escape Loops
该研究扩展了带故障模式的容错多方会话类型FTMPST，新增无需全局协调、带非阻塞退出消息的全局跳出容错循环结构，并通过旋转协调器算法变体验证了方法的可行性，为容错分布式算法的属性验证提供支持。
2025-10-28 cs.DC cs.LO
Precise subtyping for synchronous multiparty sessions
子类型的概念在理论和应用领域都有重要的作用：在lambda和并发演算以及程序设计语言中。健全性和完整性，一起被称为子类型的精确性，可以从两个不同的角度来考虑：操作和指称。前一种精确性最近在类型安全方面得到了发展，即当一个更大类型的项被期望时，一个更小类型的项的安全替换。后者的精确性是基于一个类型的外延，这是一个数学对象，它根据语言中其他表达式的外延来描述该类型的含义。本文的结果是一个同步多方会话演算的子类型的操作和指称的精确性。本文的创新之处在于引入了特征全局类型来证明运算完备性。
2016-02-11 cs.LO cs.PL
Asynchronous Sessions with Input Races
我们提出了一个演算的异步多方会话中的输入选择与不同的paths是允许的过程。我们提出了一个类型系统，接受这样的输入比赛，只要他们不妨碍锁自由。
2022-03-24 cs.LO
Towards Multiparty Session Types for Highly-Concurrent and Fault-Tolerant Web Applications
BNP Paribas（法国巴黎银行）；Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG（格勒诺布尔阿尔卑斯大学、Inria、CNRS、Grenoble INP、LIG）
本文提出一种全局类型框架，为多方会话类型添加显式失败语义和动态参与，以支持高并发和容错Web应用的正式验证。
2026-04-08 cs.LO cs.PL
Crash-Stop Failures in Asynchronous Multiparty Session Types
针对现实分布式系统中的崩溃故障，提出一种带崩溃停止语义的异步多参与方会话类型理论，通过崩溃处理分支和可选可靠性假设，保证良类型进程的无死锁、协议一致性与活性。
2025-04-17 cs.LO cs.PL
Multiparty Classical Choreographies
我们提出了多方经典编排（MCC），一个语言模型的通信系统（编排）实现类型化多方会话的全球描述。类型化是通过将经典线性逻辑推广到通过超序列明确记录并行性的判断来实现的。我们的方法将不同的工作线统一到编排和多方会议的过程中，以及它们与线性逻辑的连接。因此，在一种情况下取得的成果会转移到其他情况下。MCC的主要创新包括对编排中的服务器调用的支持，以及对具有复制流程的编排的逻辑驱动编译。
2018-12-02 cs.LO cs.PL
Reversing Single Sessions
基于会话的通信在实践中作为通过结构化交互开发安全通信系统的手段已经获得了广泛的接受。在本文中，我们研究这些结构化的相互作用是如何受到可逆性，它提供了一个计算模型，允许执行的相互作用被撤消的影响。特别是，我们提供了一个系统的研究，在两个二元和多方的单一会话的可逆性的不同概念的整合。考虑的可逆性形式是：一个是用一个向后的步骤完全反转给定的会话，另一个是用一个向后的步骤或多个步骤恢复会话的任何中间状态。我们分析了在所有这些不同的设置中逆转会话的成本。我们的研究结果表明，扩展二进制单会话多方的不影响可逆性机械及其成本。
2016-04-08 cs.LO cs.PL
Checkpoint-based rollback recovery in session programming
针对以通信为核心的系统中需撤销异常交互的需求，提出一种带会话提交、回滚、中止功能的语言，通过MAUDE实现的类型级合规检查静态避免不当回滚，满足会话无错性和进展性。
2025-01-09 cs.LO cs.PL
Causal Consistency for Reversible Multiparty Protocols
本文扩展了基于监视器即记忆的方法，为支持多方协议、异步通信、解耦回滚和抽象传递的进程模型定义了可逆语义，并证明了该语义具有因果一致性。
2021-09-30 cs.LO
Compliance for reversible client/server interactions
在会话行为的设置中，我们研究了遵守的概念的扩展时，一个纪律严明的形式回溯。在会话行为的语法中添加检查点后，我们通过LTS形式化了操作语义，并定义了检查点合规性的自然概念。然后，我们得到一个共归纳的特点，这样的顺应关系，并证明是健全的和完整的公理化表示。作为一个副产品，我们得到了一个新的顺应性的决策过程，是公理系统算法。
2014-08-26 cs.LO
Embedding Session Types in HML
最近的工作是用逻辑注释增强多方会话类型，从而能够有效地验证以下属性：（1）会话的结构，（2）消息的种类，以及（3）交换的实际值。在[3]中，我们扩展了这项工作，以实现多个跨会话交互的相互影响的规范和验证。在这里，我们给出了一个声音和完整的嵌入到Hennessy-Milner逻辑，以证明[3]中的方法的表达能力，并为它提供一个逻辑背景，使我们能够将其与类似的方法进行比较。
2013-12-10 cs.DC cs.LO
A Decentralized Analysis of Multiparty Protocols
协议在今天的并发和分布式软件中提供了统一的粘合剂;验证消息传递程序是否符合这样的管理协议是重要但困难的。基于多方会话类型（MPST）的静态方法使用协议作为类型，以避免程序中的协议违反和死锁。MPST的一个难以捉摸的问题是，以确保协议的一致性和死锁自由的实现与交叉和委托协议。我们提出了一个分散的分析多方协议，指定为全球类型和实现的异步$π$演算的交互过程。我们的解决方案依赖于两个新的概念：路由器进程和相对类型。虽然路由器进程使用全局类型来实现任意进程网络中的参与者实现的组合，但相对类型从全局类型中提取参与者对之间的预期交互和依赖关系。在我们的分析中，进程类型使用APCP，类型系统，确保协议的一致性和死锁自由二进制协议，在以前的工作中开发。我们的分散，基于路由器的分析，使健全和完整的转移协议的一致性和死锁自由从APCP多方协议。
2022-05-23 cs.LO cs.PL
Parallel Monitors for Self-adaptive Sessions
本文提出了一种数据驱动的多方会话自适应模型。系统编排由全局类型规定。参与者通过与监视器相关联的进程来体现，监视器控制参与者的行为。每个参与者都可以访问和修改一组全球数据，这些数据能够在价值观发生重大变化时触发调整。使用并行组合来构建全局类型、监视器和进程可以实现很大程度的灵活性：适配步骤可以动态地重新配置一组参与者，而不改变其余的参与者，即使两组进行通信。
2016-06-20 cs.DC cs.LO
Deconfined Global Types for Asynchronous Sessions
本文提出一种改进的异步多参与者会话类型系统，在满足良构条件时保留主体归约、会话保真和进展性质，并配有健全完备的类型推断算法，通过检查良构条件的受限形式恢复类型化的有效性。
2023-01-12 cs.LO cs.PL
Correctly Communicating Software: Distributed, Asynchronous, and Beyond (extended version)
本论文以会话类型的逻辑基础为核心，研究如何在保证正确性的前提下扩展二元与多方会话类型的表达力及适用范围，以支撑分布式异步消息传递软件的可靠验证。
2024-03-01 cs.LO
On the Impact of the Communication Model on Realisability
Université Côte d’Azur（蔚蓝海岸大学）
本文研究了不同通信模型对多方会话类型中可实现性的影响，提出统一框架并设计了不同复杂度的决策程序。
2025-12-05 cs.FL cs.LO
