Reversible Multiparty Sessions with Checkpoints
可逆的相互作用模拟不同的场景，如生化系统和人类以及自动谈判。我们抽象的互动通过多方会话丰富的命名检查点。计算可以前进或回滚到某些检查点，在这些检查点可能会采取不同的选择。通过这种方式，可以取消通信，并尝试不同的对话。交互使用全局类型进行类型化，这些类型也控制回滚。与全局类型一致的会话参与者的可类型性确保了会话保真度和可逆通信的进展。
2016-08-10 cs.LO
Partial Typing for Asynchronous Multiparty Sessions
本文针对并发系统验证难以局部化的问题，提出异步多方会话的部分类型指派系统，并证明其可类型性保证部分锁自由与孤儿消息自由。
2024-10-01 cs.LO
Multiparty Sessions based on Proof Nets
我们解释线性逻辑证明网的术语语言的基础上Solos演算。该系统包括一个同步机制，通过逻辑的保守扩展获得，能够定义非确定性行为和多方会话。
2014-06-13 cs.LO cs.PL
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
Fair Termination of Multiparty Sessions
存在一个广泛的多方会话家族，其中一个会话参与者的进展不是无条件的，而是取决于其他参与者执行的选择。这些会话不属于当前可用的保证进度的会话类型系统的范围。在这项工作中，我们提出了第一个类型系统，确保良好类型的多方会话，包括那些表现出上述依赖关系，公平地终止。公平终止是在公平假设下的终止，该假设忽略了那些被认为不公平因而不现实的互动。公平终止与会话内确保的通常的安全属性相结合，不仅本身是期望的，而且它需要进步并实现静态分析的组合形式，使得公平终止会话的良好类型的组合导致公平终止程序。
2022-05-18 cs.LO cs.PL
FTMPST: Fault-Tolerant Multiparty Session Types
本文扩展多方会话类型以集成容错机制，应对不可靠通信和进程崩溃等系统故障，并通过故障模式增强进程语义，成功应用于分析Chandra和Toueg的旋转协调器算法变体。
2023-11-24 cs.LO
Parameterised Multiparty Session Types
对于许多应用级分布式协议和并行算法，参与者的集合、消息的数量或交互结构仅在运行时才知道。本文提出了一个多方会话的依赖类型论，它可以静态地保证类型安全的，无死锁的多方进程之间的互动，其规格由索引参数化。我们使用哥德尔系统T中的原始递归运算符来表达广泛的通信模式，同时保持类型检查的可判定性。为了对单个分布式进程进行类型化，将参数化的全局类型投影到表示所有可能的端点类型的类的通用生成器上。我们证明了终止的类型检查算法在整个系统与多方会话类型和递归类型。我们说明了我们的类型论通过非平凡的编程和验证的例子，从并行算法和Web服务用例。
2012-10-10 cs.LO
Imprecise Probability for Multiparty Session Types in Process Algebra
在本文中，我们引入不精确的概率会话类型。更确切地说，我们使用的概率过程演算，其中考虑了非确定性的外部选择和概率性的内部选择。我们提出的概率多方会话类型能够编纂的通信结构，通过使用一些不精确的概率方面的下限和上限的概率。我们证明了这个新的概率分型系统是健全的，以及其他几个结果处理经典和概率性质。该方法说明了一个简单的例子，启发调查民意调查。
2020-02-19 cs.LO math.PR
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
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
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
A Logical Interpretation of Asynchronous Multiparty Compatibility
本文在命题即类型框架下将多方兼容性的相干性条件推广为转发器，并证明转发器完全刻画所有类型良好的多方兼容进程。
2023-05-25 cs.LO
Precise subtyping for synchronous multiparty sessions
子类型的概念在理论和应用领域都有重要的作用：在lambda和并发演算以及程序设计语言中。健全性和完整性，一起被称为子类型的精确性，可以从两个不同的角度来考虑：操作和指称。前一种精确性最近在类型安全方面得到了发展，即当一个更大类型的项被期望时，一个更小类型的项的安全替换。后者的精确性是基于一个类型的外延，这是一个数学对象，它根据语言中其他表达式的外延来描述该类型的含义。本文的结果是一个同步多方会话演算的子类型的操作和指称的精确性。本文的创新之处在于引入了特征全局类型来证明运算完备性。
2016-02-11 cs.LO cs.PL
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
Globally Governed Session Semantics
本文提出了一种基于多方会话类型的互模拟理论，其中编排规范管理会话类型进程及其观察者的行为。互模拟的定义与观察者与所观察到的进程合作，以形成完整的全局会话场景，并可用于证明全局协调线程和进程的优化的正确性。诱导互模拟比标准会话互模拟严格地更细粒度。只有当存在两个以上的交错多方会话时，受控制的互模拟和标准互模拟之间的差异才会出现。这个独特的功能使得能够在大规模分布式系统中推理真实场景，其中多个编排会话需要交错。通过关于受支配的基于约简的同余的可靠性和完备性，证明了受支配的双相似性的组合性。最后，在一个大规模网络基础架构的实际应用中，通过一个多会话控制下的线程转换演示了该方法的使用。
2015-03-01 cs.LO
Compositional Interface Refinement Through Subtyping in Probabilistic Session Types
本文提出概率混合选择多方会话π演算及其灵活子类型系统，允许用多个通道细化单个接口，并证明主体归约、无错误性和无死锁性，从而支持概率分布式通信的组合式验证与逐步细化。
2025-09-12 cs.LO
Embedding Session Types in HML
最近的工作是用逻辑注释增强多方会话类型，从而能够有效地验证以下属性：（1）会话的结构，（2）消息的种类，以及（3）交换的实际值。在[3]中，我们扩展了这项工作，以实现多个跨会话交互的相互影响的规范和验证。在这里，我们给出了一个声音和完整的嵌入到Hennessy-Milner逻辑，以证明[3]中的方法的表达能力，并为它提供一个逻辑背景，使我们能够将其与类似的方法进行比较。
2013-12-10 cs.DC cs.LO
Asynchronous Sessions with Input Races
我们提出了一个演算的异步多方会话中的输入选择与不同的paths是允许的过程。我们提出了一个类型系统，接受这样的输入比赛，只要他们不妨碍锁自由。
2022-03-24 cs.LO
Self-Adaptation and Secure Information Flow in Multiparty Structured Communications: A Unified Perspective
我们提出了一个全面的结构化通信模型，其中自适应和安全问题共同解决的初步结果。更具体地说，我们提出了一个模型的自适应，多方通信的安全信息流的保证。在此模型中，当进程试图在定向交换中读取或写入不适当的安全级别的消息时，就会发生安全违规。这样的违反触发适配机制，该适配机制防止违反发生和/或在编排中传播它们的影响。我们的模型配备了本地和全局机制，用于对安全违规行为做出反应;类型可靠性结果确保全局协议仍然正确执行，同时系统自适应以保持安全性。
2014-08-26 cs.CR cs.LO cs.PL
Choreography Synthesis as Contract Agreement
我们提出了一个分布式系统的正式模型，每个参与者都将其要求和义务作为行为合同，当一组合同允许合成编排时，多方会话开始。我们的框架是基于CO2演算面向合同的计算，并借用会话类型的文献的概念和结果。它支持参与者的数量没有事先确定的会话，并保持CO2的能力，以排除那些在运行时没有履行合同的参与者。我们表明，由于参与者的诚实，我们在CO2中取得了进展和会话保真度-即，他们总是遵守合同的能力。
2013-10-17 cs.DC cs.LO
Computer-aided proofs for multiparty computation with active security
安全多方计算（MPC）是一种通用的加密技术，它允许不信任方计算他们各自输入的函数，而只显示函数的输出。它已经在拍卖、电子邮件过滤和安全电话会议等领域得到了应用。鉴于其重要性，正确指定和实现协议至关重要。在程序设计语言社区中，使用计算机证明助手来验证正确性证明已经成为一种良好的实践。在密码学领域，EasyCrypt是最先进的证明助手。它为概率编程提供了一种嵌入式语言，以及嵌入到环境通用高阶逻辑中的专用逻辑。它允许我们方便地表达密码学性质。EasyCrypt已成功应用于许多应用，包括公钥加密、签名、乱码电路和差分隐私。在这里，我们第一次表明，它也可以用来证明MPC对恶意对手的安全性。我们正式添加和复制的秘密共享计划，并将其应用到毛雷尔的MPC协议的安全加法和乘法。我们的方法扩展到一般的多项式函数。我们遵循EasyCrypt的见解，即安全证明通常可以简化为关于程序等价性的证明，这是一个在程序设计语言验证中很好理解的主题。特别是，我们表明，在被动的情况下，基于非干扰的定义是相当于一个标准的基于游戏的安全定义。对于主动情况，我们提供了一个新的NI定义，我们称之为输入独立性。
2018-06-19 cs.CR cs.LO
