Denotational reasoning for asynchronous multiparty session types
University of Oxford（牛津大学）
本文首次为异步多方会话类型提供指称语义，通过精确的异步子类型化，实现对非阻塞消息传递的推理，证明通信优化的正确性，特别是消息重排序的正确性。
2026-04-12 cs.PL
Multiparty Session Types with a Bang!
本文提出带复制与一等角色的多方会话类型演算 MPST!，证明复制与递归互补可表达上下文无关及含互斥竞争的协议，并探讨其对类型检查可判定性的影响。
2025-01-24 cs.PL
Monitoring Blackbox Implementations of Multiparty Session Protocols
该研究提出分布式监控框架，支持黑盒组件的多方会话协议监控，合成监控器并证明其可靠性与透明性，扩展了可监控协议范围。
2023-10-03 cs.PL
Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Extended version)
人类的易犯错性，不可预测的操作环境以及硬件设备的异构性正在推动软件能够适应物联网或电信网络的需求。不幸的是，主流程序设计语言不容易允许软件组件通过发现、替换并与不是原始系统设计的一部分的组件通信来感测并响应于其操作环境，同时保持静态正确性保证。特别是，如果在运行时发现新组件，则不能保证其通信行为与现有组件兼容。我们通过使用具有显式连接操作的多方会话类型来解决这个问题，这是一种用于对分布式通信协议建模的类型形式。通过将会话类型与软件组件相关联，发现过程可以检查协议兼容性，并且在需要时正确地替换组件而不会危及安全性。我们提出的设计和实现的EnsembleS，第一个演员为基础的语言与自适应功能和静态会话类型系统，并将其应用到一个案例研究的基础上自适应DNS服务器。我们正式的类型系统的EnsembleS和证明的安全性良好的类型的程序，利用非经典的多方会话类型的最新进展。
2021-05-14 cs.PL
Multiparty Sessions based on Proof Nets
我们解释线性逻辑证明网的术语语言的基础上Solos演算。该系统包括一个同步机制，通过逻辑的保守扩展获得，能够定义非确定性行为和多方会话。
2014-06-13 cs.LO cs.PL
Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types
通信系统包括跨网络的各种软件组件。为了确保它们的鲁棒性，现代程序设计语言（如Rust）提供了强类型通道（其使用保证是仿射的（最多一次））和二进制通道上的取消操作。为了协调组件正确地相互通信和同步，我们使用多方会话类型的结构化机制，用仿射通信信道和隐式/显式取消机制对其进行扩展。这种新的类型规则，仿射多方会话类型（AMPST），确保取消终止多个独立运行的组件，并保证通信不会由于错误或突然终止而卡住。在AMPST的指导下，我们实现了一个与取消终止算法相关的Rust API自动生成工具（MultiCrusty），Rust编译器通过该工具自动检测不安全的程序。我们的评估表明，MultiCrusty提供了一种有效的机制，用于通信，同步和传播任意进程的取消通知。我们已经实现了几个用例，包括流行的应用程序协议（OAuth，SMTP）和具有异常处理模式的协议（断路器，分布式日志记录）。
2022-04-28 cs.PL
Multiparty Session Typing, Embedded (Technical Report)
本文提出mpst.embedded库，利用Scala的match types将多方会话类型（MPST）作为内部DSL直接嵌入，从而避免了外部DSL方法的编程阻力与抽象泄漏问题。
2025-01-29 cs.PL
Fair Termination of Multiparty Sessions
存在一个广泛的多方会话家族，其中一个会话参与者的进展不是无条件的，而是取决于其他参与者执行的选择。这些会话不属于当前可用的保证进度的会话类型系统的范围。在这项工作中，我们提出了第一个类型系统，确保良好类型的多方会话，包括那些表现出上述依赖关系，公平地终止。公平终止是在公平假设下的终止，该假设忽略了那些被认为不公平因而不现实的互动。公平终止与会话内确保的通常的安全属性相结合，不仅本身是期望的，而且它需要进步并实现静态分析的组合形式，使得公平终止会话的良好类型的组合导致公平终止程序。
2022-05-18 cs.LO cs.PL
Speak Now: Safe Actor Programming with Multiparty Session Types (Extended Version)
University of Glasgow（格拉斯哥大学）；Queen Mary University of London（伦敦大学女王玛丽学院）
Maty是首个支持静态多方会话类型和多会话Actor的编程语言，通过流敏感效果系统和事件驱动编程实现通信安全与系统容错。
2026-03-03 cs.PL
Multiparty Session Programming with Global Protocol Combinators
多方会话类型（MPST）是通信协议的类型规则。它确保了良好类型的通信进程不会出现通信错误和死锁。MPST理论的最新实现依赖于（1）运行时线性检查以确保通信信道的正确使用，以及（2）用于指定和验证多方协议的外部域特定语言。为了克服这些限制，我们提出了一个用全局组合子编程的库--一组用于在OCaml中编写和验证多方协议的函数。一个协议中所有进程的局部行为都是从全局组合子中一次推断出来的。我们形式化的全球combinators和证明一个健全的可实现的全球combinators -一个良好类型的全球combinator派生出一组本地类型，类型端点程序可以确保类型和通信安全。我们的方法使全静态验证和整个协议的实现，从协议规范的过程实现，发生在同一种语言。我们将我们的实现与无类型和延续传递风格的实现进行比较，并通过实现大量的协议来展示其表现力。我们展示了我们的库可以与现有的库和服务进行互操作，实现DNS（域名服务）协议和OAuth（开放认证）协议。
2020-05-24 cs.PL
CAMP: Cost-Aware Multiparty Session Protocols
基于多方会话类型（MPST）理论，提出了一种新的消息传递并发分布式系统静态性能分析框架CAMP。了解并发和分布式系统的运行时性能对于识别瓶颈和优化机会非常重要。在消息传递设置中，这些瓶颈通常是通信开销和同步时间。尽管它的重要性，推理软件的这些内涵属性，如性能，很少受到关注，相比，验证扩展属性，如正确性。基于会话类型的行为协议规范不仅可以描述并发和分布式系统的外延性质，还可以描述并发和分布式系统的内涵性质。CAMP增强MPST与注释的通信延迟和本地计算成本，定义为估计的执行时间，我们使用的协议描述中提取成本方程。CAMP也是可扩展的，以分析建立在会话类型论的最新进展上的异步通信优化。我们将我们的工具应用于文献中不同的现有基准测试和用例，这些测试和用例具有广泛的通信协议，并在C，MPI-C，Scala，Go和OCaml中实现。我们的基准测试表明，在大多数情况下，我们预测的实际执行成本的上限误差< 15%。
2020-10-09 cs.PL
An Erlang Implementation of Multiparty Session Actors
通过使用显式消息传递而不是依赖于共享内存来进行协调，基于角色的程序设计语言已被证明是构建可靠和容错分布式系统的有效工具。虽然本质上是以通信为中心的，但基于参与者的应用程序中的通信模式仍然是非正式指定的，这意味着通信中的错误很晚才被检测到。多方会话类型是在全局级别上描述多个通信实体之间的交互的形式主义。本文描述了一个原型框架的实现，该框架用于根据多方会话类型监控Erlang/OTP gen_server应用程序，展示了如何将以前关于多方会话参与者的工作调整为纯粹基于参与者的语言，以及如何根据Erlang的“让它失败”的咒语报告会话参与者的监控违规和终止。最后，该框架是用来实现两个案例研究：适应免费提供的DNS服务器，和聊天服务器。
2016-08-11 cs.DC cs.PL
Hybrid Multiparty Session Types -- Full Version
多方会话类型（MPST）是分布式消息传递系统的规范和验证框架。系统的通信协议被指定为全局类型，通过端点投影从该全局类型获得局部类型的集合（局部流程实现）。全局类型是整个系统的单一规范实体，由一个完全了解通信协议的设计者指定。另一方面，分布式系统通常根据其组件来描述：不同的设计者负责为每个组件提供子协议。全球协议的模块化规范的问题已在文献中得到解决，但最先进的只集中在双输入/输出兼容性。我们的工作克服了这一限制。我们提出了第一个MPST理论的多方组成的分布式协议规范，是语义保持，允许组成两个或多个组件，并保留完整的MPST表现力。我们引入混合类型描述子协议相互作用，定义了一种新的兼容性关系，明确描述了一种算法组成多个子协议到一个良好的形式的全球类型，并证明组合保持投影，从而保留语义保证，如活性和死锁自由。最后，我们测试我们的工作对现实世界的案例研究，我们顺利地扩展我们的新的兼容性MPST与委托和显式连接。
2023-03-20 cs.PL
Towards Quantum Multiparty Session Types
本研究为极简多方会话类型系统扩展量子数据与操作，提出量子多方会话类型（QMPSTs），可从全局和局部层面规范量子协议并保障通信及量子特性，已验证四种经典量子协议。
2024-09-17 cs.PL
Verifying Asynchronous Interactions via Communicating Session Automata
本文提出了一个合理的过程来验证通信会话自动机（CSA）的属性，即，包括多方会话类型的通信自动机。我们引入了一个新的异步兼容性属性CSA，称为k-多方兼容性（K-MC），这是一个严格的超集的同步多方兼容性的理论和工具的基础上的会话类型。它被分解为两个有界属性：（i）一个称为k-安全性的条件，保证在界限内，所有发送的消息都可以被接收，每个自动机都可以移动;（ii）一个称为k-穷举性的条件，保证所有k-可达的发送动作都可以在界限内被触发。我们表明，k-穷举意味着存在的有界性，并健全和完整的特征系统，每个自动机的行为下的界限大于或等于k等效。我们发现，检查k-MC是PSPACE完成的，并证明其性能的经验，在大型系统中使用偏序减少。
2019-05-21 cs.PL
Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types
本文提出用精化多方会话类型描述并强制合法的消息交互序列，以防范 MAVLink 无人机协议中表面合法却可导致系统进入不安全状态的隐蔽攻击。
2025-03-14 cs.CR cs.PL
Design-by-Contract for Flexible Multiparty Session Protocols -- Extended Version
编排模型支持分布式编程中的构造纠正原则。此外，它们能够根据所需系统行为的全局规范自动生成正确的基于消息的通信模式。在本文中，我们扩展了理论的编排自动机，编排模型的基础上，有限状态自动机，有两个关键功能。首先，我们允许参与者只在编排自动机描述的某些场景中行动。虽然这看起来很自然，但文献中的许多编排方法，特别是编排自动机，禁止这种行为。其次，我们为通信配备了约束可以通信的值的断言，从而实现按契约设计的方法。我们提供了一个工具链，允许利用上述理论为TypeScript Web编程生成API。通过生成的API进行通信的程序通过构造遵循规定的通信模式，并且没有诸如死锁之类的通信错误。
2022-05-13 cs.PL
Fearless Asynchronous Communications with Timed Multiparty Session Protocols
本文提出首个基于多方会话类型的仿射性、时间约束、超时与时间故障处理形式化集成理论，静态保证异步定时通信的无死锁与无畏安全，并引入 Rust 工具链实现，验证其开销可忽略且适用于现实场景。
2024-08-30 cs.PL
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 Synthetic Reconstruction of Multiparty Session Types (with Appendix)
University of Kent（肯特大学）；Royal Holloway, University of London（伦敦大学皇家霍洛威学院）；University of Groningen（格罗宁根大学）
本文提出了一种新的多方会话类型方法，通过直接验证进程与全局协议规范，实现了表达能力和组合性的平衡。
2025-11-27 cs.PL
Deadlock-free asynchronous message reordering in Rust with multiparty session types
Rust是一种注重性能和可靠性的现代系统语言。为了补充Rust提供“无畏并发”的承诺，开发人员经常利用异步消息传递。不幸的是，任意地对发送和接收消息进行排序以最大化计算-通信重叠（对消息传递应用程序的流行优化），这打开了一个潘多拉盒子，里面有更多微妙的并发性错误。为了通过构造来保证无死锁，我们提出了Rumpsteak：一个基于多方会话类型的新Rust框架。Rust中以前的会话类型实现要么建立在同步和阻塞通信的基础上，要么局限于两方交互。至关重要的是，它们都不支持为提高效率而对消息进行任意排序。相反，Rumpsteak的目标是异步的JavaScript/await代码。它的独特功能是允许开发人员任意排序发送/接收消息，同时保持无死锁。为此，Rumpsteak结合了两个最近的高级会话类型论：（1）k-多方兼容性（kmc），它全局验证一组参与者的安全性，以及（2）异步多方会话子类型，它在单个参与者的上下文中局部验证优化。具体来说，我们提出了一种新的算法，异步子类型，是健全的和可判定的。我们首先评估Rumpsteak与之前三个Rust实现的性能和表现力。我们发现Rumpsteak的效率提高了1.7- 8.6倍，并且可以通过提供任意的消息排序来安全地表达更多的示例。其次，我们分析了我们的新算法的复杂性，并将其与kmc和二进制会话子类型算法进行了比较。我们发现它们比Rumpsteak的要慢得多…
2022-02-02 cs.PL cs.SE
Zooid: a DSL for Certified Multiparty Computation
我们设计和实现Zooid，一个特定于领域的认证多方通信的语言，嵌入在Coq和实现我们的异步多方会话类型的机械化框架（第一个）。Zooid为全局和局部类型的语义提供了一个完全机械化的元理论，以及一个完全验证的端点处理语言，它忠实地反映了类型级别的行为，从而继承了全局类型的属性，如死锁自由，协议遵从性和活性保证。
2021-03-18 cs.PL
Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
本文提出一种等递归GMST类型系统，通过名为合规性的终止函数计算环境行为属性，解决了传统等递归方法机械化复杂和依赖模型检查器的问题，并在OCaml中实现和自动化验证了无死锁与无不匹配特性。
2025-01-29 cs.PL
Comprehensive Multiparty Session Types
多方会话类型（MST）是一种成熟的类型论，它从全局的角度描述了固定数量组件的交互结构，并通过将全局类型投影到会话的参与者上来对组件进行类型检查。它们保证多方会话（LMS）语言的通信安全，即，分布式并行组件可以在没有死锁和意外消息类型的情况下交换值。已经提出了MST和LMS的几个变体来研究分布式和并行编程的关键特征。我们观察到所考虑的变体的群体仅来自一个祖先，即，原始LMS/MST，并且所考虑的变体和原始的特征之间存在重叠的特征。这些因素阻碍了会议类型和语言的演变及其在实践中的采用。本文讨论了以下问题：什么是MST和LMS的基本功能，以及如何用简单的结构来建模？据我们所知，这是第一次讨论这个问题。我们对MST、LMS和所考虑的变体中的特征和结构进行了系统的分析，以确定基本特征。这些变体是最有影响力的（根据Google Scholar）和完善的系统之一，涵盖了分布式并行编程的广泛领域。我们使用经典的形式化模型技术，如BNF，结构一致性，小步操作语义和类型判断来构建我们的语言和类型系统。最后，通过归纳证明了操作语义与类型系统的一致性。本文提出了一组基本特征、一种结构化交互语言和一种综合多方会话类型的类型论，包括全局类型和类型系统。该分析去除了重叠的特征并捕获了共享的特征，从而引入了基本特征。该语言的结构简单而基本，基于$λ$和$π$演算。类似地，我们的全局类型反映了语言中省略和引入的内容…
2019-02-01 cs.PL
Precise subtyping for synchronous multiparty sessions
子类型的概念在理论和应用领域都有重要的作用：在lambda和并发演算以及程序设计语言中。健全性和完整性，一起被称为子类型的精确性，可以从两个不同的角度来考虑：操作和指称。前一种精确性最近在类型安全方面得到了发展，即当一个更大类型的项被期望时，一个更小类型的项的安全替换。后者的精确性是基于一个类型的外延，这是一个数学对象，它根据语言中其他表达式的外延来描述该类型的含义。本文的结果是一个同步多方会话演算的子类型的操作和指称的精确性。本文的创新之处在于引入了特征全局类型来证明运算完备性。
2016-02-11 cs.LO cs.PL
Communication-Safe Web Programming in TypeScript with Routed Multiparty Session Types
现代网络编程涉及协调浏览器客户端和服务器之间的交互。通常，基于Web的分布式系统中的交互是非正式描述的，这使得很难确保正确性，特别是通信安全性，即所有端点都没有类型错误或死锁，符合指定的协议。我们提出了STScript，一个工具链，它生成TypeScript API，用于通过WebSockets进行通信安全的Web开发，以及RouST，一种新的会话类型论，支持具有路由机制的多方通信。STScript为开发人员提供了基于RouST的通信协议规范生成的TypeScript API。生成的API建立在TypeScript并发实践的基础上，补充了全栈Web开发中的事件驱动编程风格，并且与服务器端端点的Node.js运行时和浏览器端端点的React.js框架兼容。RouST可以表达通过中间参与者路由的多方交互。它支持浏览器端端点之间的对等通信，通过服务器路由通信，避免过度序列化。RouST保证使用STScript API编写的端点Web应用程序的通信安全。我们使用几个部署为Web应用程序的生产就绪的案例研究来评估STScript对现代Web编程的表现力。
2021-01-12 cs.PL cs.SE
Synthesising Choreographies from Local Session Types (extended version)
设计和分析多方分布式交互可以通过全局视图（例如基于编排的方法）或通过组成可用的计算实体（例如服务编排）来实现。本文提出了一种类型化系统，它允许在某些条件下，从一组描述端点行为（即本地类型）的本地会话类型中合成编排（即多方全局类型）。
2012-04-11 cs.DC cs.PL
Multiparty Symmetric Sum Types
本文介绍了一种新的基于对称和类型的多方会话类型的理论，我们可以类型的非确定性的编排选择行为。虽然会话类型中的原始分支类型可以表示由单个参与者做出并被其他参与者接受的决定会话如何进行的选择，但对称和类型表示由会话的所有参与者之间的协议做出的选择。这种行为可以在许多实际系统中找到，包括用于临床实践指南（CPG）的医疗保健系统中的协作工作流。使用对称和的过程可以嵌入到使用导体过程的原始分支类型中。我们表明，这种类型驱动的嵌入保留类型，满足语义的健全性和完整性，并满足编码标准适应类型设置。该理论导致了一个有效的实现的原型工具，自动翻译的原始CPG规范从一个表示称为过程矩阵的对称和类型，类型检查程序，并执行它们。
2010-11-30 cs.DC cs.PL
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
本文比较多方会话类型(MPST)的自顶向下和自底向上方法，通过构建基于图表示的新算法进行详细复杂性分析，发现自顶向下方法在多数实际场景中更高效，而自底向上的活性检查和类型推断复杂性较高。
2024-11-12 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
Mixed Choice in Asynchronous Multiparty Session Types
University of Kent（肯特大学）；Queen Mary University of London（伦敦大学玛丽女王学院）；University of Glasgow（格拉斯哥大学）
本文提出了一种支持异步混合选择的多党会话类型框架，并通过工具链验证了其正确性。
2026-09-28 cs.DC cs.FL cs.MA
Generalising Projection in Asynchronous Multiparty Session Types
多方会话类型（MST）为指定和验证消息传递软件系统提供了一种有效的方法。在MST理论中，全局类型指定了全局级别上角色之间的交互。每个角色的本地规范是通过从全局类型投射到它所参与的消息交换上来生成的。只要一个全局类型可以被投射到每个角色上，投射的组合就没有死锁，并且具有全局类型所指定的行为。MST可用性的关键是投影操作：更具表达性的投影允许更多的系统进行类型检查，但需要更困难的合理性参数。在本文中，我们推广的标准投影操作MST。这使我们能够对分布式系统中的许多设计模式进行建模和类型检查，例如标准投影所拒绝的负载均衡。新预测的关键是跟踪信息之间因果关系的分析。我们的合理性证明使用新的图论技术从消息序列图的理论。我们展示了新的投影操作的有效性，显示了许多全球类型的共同模式，可以根据我们的投影，但不是根据标准的投影操作。
2022-08-10 cs.FL cs.PL
Complete Multiparty Session Type Projection with Automata
提出首个可靠、完备且高效的MST投影算子，分离合成与可实现性检查，证明MST可实现性属于PSPACE，改进了先前EXPSPACE的结果，并通过原型实现验证了有效性。
2024-03-27 cs.DC cs.FL cs.PL
Statically Verified Refinements for Multiparty Protocols
随着分布式计算在现代变得无处不在，安全的分布式编程是一个公开的挑战。为了解决这个问题，多方会话类型（MPST）为消息传递并发提供了一个类型规则，保证了通信安全属性，如死锁自由。虽然最初MPST集中在通信方面，并采用一个简单的类型系统的通信有效载荷，在现实世界中的通信协议通常包含的有效载荷的约束。我们介绍了改进的多方会话类型（RMPST），MPST的扩展，通过细化类型的数据类型表示数据相关的协议。我们提供了一个RMPST的实现，在一个工具链称为会话 *，使用Scribble，多方协议描述工具链，并针对F*，面向验证的功能程序设计语言。用户可以在Scribble中描述协议，并使用从协议生成的精炼类型的API在F* 中实现端点。然后F* 编译器可以静态地验证细化。此外，我们使用一种新的回调风格的API生成方法，提供静态线性保证与控制反转。我们评估我们的方法与现实世界的例子，并表明，它几乎没有开销相比，一个天真的实现，同时保证从底层理论的安全属性。
2020-09-14 cs.DC cs.PL
Multiparty Session Type-safe Web Development with Static Linearity
现代Web应用程序现在可以在浏览器内提供类似桌面的体验，这要归功于WebSockets等技术，这些技术可以在浏览器和服务器之间实现低延迟双工通信。虽然这些进步对用户体验来说是巨大的，但它们代表了Web开发人员的新责任，他们现在需要管理和验证应用程序中更复杂和可能有状态的交互的正确性。在本文中，我们提出了一种技术，用于开发交互式Web应用程序，静态保证通信遵循给定的协议。首先，用Scribble协议语言描述全局交互协议--基于多方会话类型。Scribble协议被检查为格式良好，然后每个角色被投射到一个有限状态机，从角色的角度表示通信的结构。我们使用源代码生成和一种新的类型级编码的FSM使用多参数类型类，以利用类型系统的目标语言，并保证只有程序的通信协议将类型检查。我们的工作目标是PureScript --一种编译为JavaScript的函数式语言--它具有足够的表达能力来提供静态线性保证。我们证明了我们的方法的有效性，通过基于Web的战舰游戏，通过WebSocket连接进行通信。
2019-04-02 cs.PL cs.SE
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures
针对分布式系统故障，提出Teatrino工具链，基于崩溃停止语义的异步多方会话类型，扩展Scribble和Effpi生成协议一致的Scala代码，保证无死锁、一致性和活性。
2023-05-15 cs.DC cs.PL
Recursive Session Types Revisited
会话类型为基于通信的结构化编程建模。具体来说，π演算的二进制会话类型描述了分布式场景中两个参与者之间的通信。向pi演算添加会话意味着用类型和术语构造来扩充它。在之前的一篇文章中，我们试图理解会话结构在何种程度上比标准的pi演算结构更复杂和更具表达力。为此，我们采用线性类型和变量类型以及连续传递原则，提出了一种将二进制会话pi演算编码为标准类型pi演算的方法。在本文中，我们专注于递归会话类型，我们提出了一个编码到递归线性π演算。这种编码是前者的保守扩展，因为它保留了其中获得的结果。最重要的是，它采用了对偶关系的新处理方法，在递归类型的情况下，这已经被证明是相当具有挑战性的。
2014-08-26 cs.PL
Asynchronous Multiparty Session Type Implementability is Decidable -- Lessons Learned from Message Sequence Charts
该研究解决了具有发送方驱动选择的异步多方会话类型可实现性的可判定性开放问题，通过推广高级消息序列图的结论给出肯定答案，同时研究了相关技术适配并证明了一类推广的可实现性问题不可判定。
2023-07-18 cs.DC cs.FL cs.PL
Refinements for Multiparty Message-Passing Protocols: Specification-agnostic theory and implementation
本文提出规范无关的多参与方消息传递协议精化框架及Rust实现，通过精化迹系统和RCS计算模型解耦正确性与规范格式，并验证其灵活性与低开销。
2024-08-09 cs.PL
MAG$π$!: The Role of Replication in Typing Failure-Prone Communication
本文提出MAG$π$!扩展，首次将复制构造引入多方会话类型（MPST）并提升至类型级别，简化了分布式客户端-服务器交互规范，同时证明了主语归约、会话保真等性质。
2024-04-24 cs.PL
Session Types Go Dynamic or How to Verify Your Python Conversations
本文介绍了动态类型语言Python中会话类型的第一个实现。整个系统的通信安全在运行时由监视器保证，监视器检查执行跟踪是否符合相关协议。协议是用Scribble编写的，Scribble是一种基于多方会话类型的编排描述语言，添加了逻辑公式以获得更精确的行为属性。所提出的框架克服了以前的工作的局限性，所有端点的会话类型应该是静态类型的，使他们不允许与无类型的参与者的互操作性。通过用例和基准测试，展示了动态协议检测的优势、表现力和性能。
2013-12-10 cs.PL
An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
提出基于自动机的多方协议框架AMP，引入协议状态机与通信状态机规范，并提供完备的PSPACE投影操作与类型系统，显著提升了Multiparty Session Types的表达性、解耦性与鲁棒性。
2025-01-28 cs.FL cs.PL
Session Communication and Integration
大型分布式系统的基于CORBA的规范通常被自然地分解成各种模块。规范模块的集成与程序组件的并行组合形成对比，并且包括各种方式，例如场景连接、选择和嵌套。最近开发的多方会话类型的过程演算提供了有用的技术，以适应协议模块化，通过编码的通信协议的片段中使用的私人通道一类的代理。在本文中，我们扩展了前面的会话类型论，通过增强会话集成机制。更具体地说，我们提出了一种新的同步多方会话类型论，其中会话分为通信和集成的水平。通信会话记录了多个代理之间基于消息的通信，而集成会话描述了通信会话的集成。本文提出了一个两级的会话类型系统，并研究了该类型系统的一些关键性质。应用该理论的系统描述，我们表明，通道的安全性和会话一致性属性可以分析。同时，为了提高理论的实用性，在类型检查中使用进程切片的方法来帮助识别违规会话。
2012-10-08 cs.PL cs.SE
kmclib: Automated Inference and Verification of Session Types
基于多方会话类型的理论和工具为使用消息传递进行通信的并发程序提供了正确性保证。这些保证通常以本质上自顶向下的方法为代价，这种方法需要将整个程序的通信行为指定为全局类型。本文介绍了kmclib：一个OCaml库，它支持开发正确的消息传递程序，而无需编写任何类型。该库利用OCaml的元编程工具来自动推断并发程序的会话类型并验证其兼容性（k-MC）。用kmclib编写的类型良好的程序不会导致通信错误，也不会卡住。
2021-11-26 cs.PL
Undecidability of Asynchronous Session Subtyping
会话类型用于描述分布式系统中的通信协议，并且通常在类型论中，会话子类型化表征通信过程的可替换性。我们调查（联合国）的可判定性的会话类型在异步通信系统。我们首先设计了一个核心的不可判定的子类型关系，通过对类型的结构施加限制。然后，作为这个初始不可判定性结果的结果，我们表明（不同于文献中所述或所述的）到目前为止为会话类型定义的异步子类型的三个概念都是不可判定的。也就是说，我们认为异步会话子类型的Moonlight和Yoshida的二进制会话，陈等人的关系。二进制会话的假设下，发出的每一个消息最终消费，和一个Moonlight等人。多方会话类型。最后，通过证明核心子类型关系的两个片段是可判定的，我们证明了对类型结构的进一步限制使我们的核心子类型关系是可判定的。
2017-07-19 cs.PL
Forwarders as Process Compatibility, Logically
会话类型定义进程在通信时必须遵循的协议。二元会话类型的特殊情况，即双方之间协议的类型注释，已知与线性逻辑处于命题类型对应关系中。在以前的工作中，我们已经表明，泛化到多方会话类型可以表示一致性证明或仲裁器，根据给定的协议转发消息作为中间件的过程。在本文中，按照命题作为类型的方式，我们推广到一个逻辑，我们称之为转发逻辑，一个片段的经典线性逻辑仍然满足割消。我们的主要结果总结如下：转发器推广一致性，并给出了一个优雅的证明理论的多方兼容性，并发系统的属性，保证所有发送的消息最终收到，没有死锁发生的表征。
2021-12-14 cs.LO cs.PL
Top-down = Bottom-up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols
University of Oxford（牛津大学）
研究多方会话类型中自上而下与自下而上策略的可类型化性，通过主全局类型推断算法证明二者相同，实现相关算法并构建工具链，经评估发现自上而下方法比自下而上方法更高效。
2026-07-24 cs.PL
MAG$π$: Types for Failure-Prone Communication
多方会话类型（MPST）是一种用于以通信为中心的系统的类型规则，可以保证通信安全、无死锁和协议遵从性。已经出现了几个工程模型的故障，并引入容错技术。然而，这样的工作经常对底层网络做出假设，例如，基于TCP的通信，保证消息的传递;或者采用集中的可靠节点和ad-hoc可靠性概念;或者只解决单一类型的故障，例如节点崩溃故障。在这项工作中，我们开发了MAG $π$ --一个多方、异步和通用的$π$演算，它是第一个语言和类型系统，以适应一致：（i）最广泛的非拜占庭故障，包括消息丢失、延迟和重新排序;崩溃故障和链路故障;和网络分区;（ii）一个新的和最普遍的概念的可靠性，考虑到每个参与者的观点，在协议;（iii）频谱的网络假设从最低的UDP为基础的网络编程的TCP为基础的应用程序的水平。我们证明了主题约简和会话保真度;进程属性（死锁自由，终止等）;故障处理的安全性和可靠性。
2023-01-25 cs.PL
A Decentralized Analysis of Multiparty Protocols
协议在今天的并发和分布式软件中提供了统一的粘合剂;验证消息传递程序是否符合这样的管理协议是重要但困难的。基于多方会话类型（MPST）的静态方法使用协议作为类型，以避免程序中的协议违反和死锁。MPST的一个难以捉摸的问题是，以确保协议的一致性和死锁自由的实现与交叉和委托协议。我们提出了一个分散的分析多方协议，指定为全球类型和实现的异步$π$演算的交互过程。我们的解决方案依赖于两个新的概念：路由器进程和相对类型。虽然路由器进程使用全局类型来实现任意进程网络中的参与者实现的组合，但相对类型从全局类型中提取参与者对之间的预期交互和依赖关系。在我们的分析中，进程类型使用APCP，类型系统，确保协议的一致性和死锁自由二进制协议，在以前的工作中开发。我们的分散，基于路由器的分析，使健全和完整的转移协议的一致性和死锁自由从APCP多方协议。
2022-05-23 cs.LO cs.PL
Session Types With Multiple Senders Single Receiver (report version)
本文通过引入存在分支类型扩展了会话类型，以支持同步设置下多发送方单接收方的交互模式，并构建了保证类型安全、无死锁和保真性的类型系统，同时提供新通信类型系统保证动态交错多方会话进展性，最后将Rust多线程原语编码入该系统以验证其表达能力。
2023-10-20 cs.PL
