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
Domain-Aware Session Types (Extended Version)
我们开发了一个泛化现有的Curry-Howard解释（二进制）会话类型依赖于线性逻辑的扩展与混合逻辑的功能，特别是模态世界，表明域。这些世界支配着域迁移，服从于模态逻辑的Kripke语义中熟悉的参数可访问性关系。其结果是一个富有表现力的新型流程框架，用于域感知、消息传递并发。它的逻辑基础确保良好类型的进程享有会话保真度、全局进展和终止。类型化还确保进程只与可访问域通信，因此尊重可访问性关系。值得注意的是，我们的域感知框架可以指定的情况下，域信息仅在运行时可用，灵活的可访问性关系可以干净地定义和静态执行。作为一个具体的应用，我们引入了域感知的多方会话类型，其中全局协议可以通过域迁移来表示任意嵌套的子协议。我们开发了一个精确的分析，这些多方协议减少到我们的二进制域感知框架：复杂的域感知协议可以推理在正确的抽象层次，也确保了原则性转移的关键正确性属性从二进制到多方设置。
2019-07-02 cs.LO
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
Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom
我们研究不同的公平性假设如何影响锁自由，一个典型的会话类型系统的活性属性为目标的结果。我们修复了一个最小的会话演算，并系统地考虑到所有已知的公平性假设，从而准确地确定三个有趣的和语义上不同的概念锁自由，所有这些都有一个健全的会话类型系统。然后，我们表明，通过使用一个通用的合并运算符，否则标准的方法来全局会话类型，我们得到一个会话类型系统完成最强的锁自由的概念，它只假设公正的执行路径，最小的公平性假设并发系统。
2021-04-29 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
Probabilities in Session Types
本文讨论了分布式系统的概率行为描述的过程演算考虑概率的内部选择和非确定性的外部选择。对于这个演算，我们定义和研究的类型系统，扩展了多方会话类型，以处理概率行为。通过一个运行的例子，对演算及其类型化系统进行了说明.
2019-09-04 cs.LO
Causal Consistency for Reversible Multiparty Protocols
本文扩展了基于监视器即记忆的方法，为支持多方协议、异步通信、解耦回滚和抽象传递的进程模型定义了可逆语义，并证明了该语义具有因果一致性。
2021-09-30 cs.LO
Forwarders as Process Compatibility, Logically
会话类型定义进程在通信时必须遵循的协议。二元会话类型的特殊情况，即双方之间协议的类型注释，已知与线性逻辑处于命题类型对应关系中。在以前的工作中，我们已经表明，泛化到多方会话类型可以表示一致性证明或仲裁器，根据给定的协议转发消息作为中间件的过程。在本文中，按照命题作为类型的方式，我们推广到一个逻辑，我们称之为转发逻辑，一个片段的经典线性逻辑仍然满足割消。我们的主要结果总结如下：转发器推广一致性，并给出了一个优雅的证明理论的多方兼容性，并发系统的属性，保证所有发送的消息最终收到，没有死锁发生的表征。
2021-12-14 cs.LO cs.PL
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
Concerto Grosso for Sessions: Fair Termination of Sessions
本文在 Agda 中机械化推理系统元理论，研究会话类型通信中的公平终止及其与无锁性的关系。
2023-07-08 cs.LO cs.PL
Synchronous Forwarders
会话类型是用于指定进程在彼此通信时必须遵循的协议的类型。会话类型与线性逻辑处于命题作为类型的对应关系中。以前的工作已经表明，多方会话类型，会话类型的两个或两个以上的缔约方的协议的概括，可以建模为一致性的证明，线性逻辑对偶的概括。而且，表示为一致性的协议可以由仲裁器模拟，仲裁器是根据给定协议转发消息的中间件。在本文中，我们将仲裁器的概念推广到同步转发器的概念，同步转发器是一个以几种不同方式实现仲裁器行为的过程。在一个命题作为类型的方式，同步转发器形成一个逻辑配备了削减消除，这是一个特殊的限制经典线性逻辑。我们的主要结果表明，同步转发器是一致性的表征，即，相干性证明可以被转换成同步转发器，反之亦然，每个同步转发器对应于一个相干性证明。
2021-02-09 cs.LO cs.PL
Towards a Semantic Characterisation of Global Type Well-formedness
本文以素事件结构为语义模型，为多方会话全局类型的可投影性和有界性提供语义刻画，并识别出良构全局类型对应PES的结构性质。
2024-04-08 cs.LO
An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $π$-Calculus
公平终止是程序的属性，这些程序可能“在原则上”偏离，但“在实践中”终止，即在关于非确定性选择的解决方案的适当公平假设下终止。我们研究了$μ$ MALL $^\infty$的一个保守扩展，$^\infty$是线性逻辑中具有最小和最大不动点的乘性加性片段的无穷证明系统，使得割消对应于公平终止。证明项是$π$ LIN的过程，它是线性$π$演算的一个变体，具有（共）递归类型，可以将二进制和（某些）多方会话编码到其中。因此，我们获得了一个行为类型系统的$π$ LIN（和间接会话演算通过其编码到$π$ LIN），确保公平终止：虽然良好的类型的进程可能会参与任意长的交互，他们是公平的保证，最终执行所有挂起的动作。
2022-07-08 cs.LO cs.PL
Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
我们提出了第一个会话类型系统，保证可能非终止通信进程的请求-响应活性属性。这些类型用一组所需的响应来扩充标准二进制会话类型的分支和选择类型，这表明每当选择特定标签时，最终也必须选择一组其他标签，即其响应。我们证明，这些扩展类型是严格的表达比标准的会话类型。我们提供了一个类型系统的过程演算类似于一个子集的内部（基于数据）和外部（基于事件）分支，消息传递，有界和无界循环的协作BPMN流程。我们证明了这个类型系统是合理的，即，它保证了无死锁进程的请求-响应活性。我们在一个无限状态系统的具体例子上说明了微积分和类型系统的使用。
2016-01-05 cs.LO
Classical Higher-Order Processes
经典过程（CP）是一种演算，其中经典线性逻辑类型的证明理论与移动通道通信过程，一个la pi演算。它的结构建立在最近的命题作为类型之间的会话类型和线性逻辑命题的对应关系。期望的属性，如在约简和进展下的类型保持，来自线性逻辑的元理论。我们有助于这一研究线扩展CP代码的流动性。我们概括了经典的线性逻辑，以捕捉高阶（线性）推理的证明，这产生了一个逻辑重建（变种）的高阶π演算（HOPI）。由此产生的演算被称为经典高阶过程（CHOP）。我们探讨CHOP的元理论，证明其语义享有类型保护和进步（条款不卡住）。我们还说明了CHOP的表现力，通过例子，派生的语法糖，并扩展到多方会议。最后，我们定义了一个从CHOP到CP的翻译，它将进程代码的移动性编码为引用传递。
2018-02-08 cs.LO cs.PL
Comparing Deadlock-Free Session Typed Processes
除了遵守规定的协议，以通信为中心的系统永远不应该“卡住”。这个需求已经通过诸如进度或（死）锁自由度之类的活动属性来表达。已经提出了几个类型的纪律，确保这些属性的移动进程。不幸的是，人们对这些规程之间的精确关系以及它们所引发的类型化过程的类知之甚少。本文对两类无死锁的会话型并发进程L和K进行了比较。类L因其规范性而突出：它自然地产生于将线性逻辑命题解释为会话类型。类K，通过将会话类型编码到Kobayashi的使用类型中获得，包括在其他类型系统中不可类型化的进程。我们证明了L严格包含在K中。我们还确定了L和K重合的精确条件。一个关键的观察是，并行进程之间的共享程度决定了类型化进程的新表达层次结构。我们还提供了一个保持类型的重写过程中的进程在K到L。这个过程表明，虽然共享程度是有效的，但它是区分类型化进程的一个相当微妙的标准。
2015-08-27 cs.LO cs.PL
Session Types as Generic Process Types
行为型系统比通常的静态分析更安全。它们基于“类型即进程”的思想，为特定的属性提供专用的类型代数，从协议兼容性到竞争自由、锁自由甚至响应性。有两种成功的方法，尽管它们有很大的不同，它们是会话类型和进程类型。前者允许使用特定类型（证明）系统来指定和验证（分布式）通信协议;后者允许从系统规范中推断出一个过程抽象，使用通用类型（证明）系统可以更简单地验证属性。这些方法之间的关系是什么？一般的一个可以substantially具体的一个？代价是什么？前者可以作为后者的编译器吗？本文介绍的工作是朝着回答这些问题迈出的一步。具体地说，我们定义了一个逐步编码的pi演算会话和会话类型（系统的盖伊和孔）到一个pi演算的进程类型（通用类型系统的五十岚和小林）。我们对会话类型环境、极性（区分会话通道端点）和标记总和进行编码。我们展示了编码的正向和反向操作对应，以及类型对应。为了在进程类型子类型中忠实地编码会话子类型，需要向目标语言添加记录构造函数和新的子类型规则。总之，作为协议抽象的会话类型的编程便利性可以与pi演算的简单性和功能相结合，特别是利用通用类型系统提供的框架。
2014-08-07 cs.LO cs.PL
Comparing Type Systems for Deadlock Freedom
消息传递软件系统表现出非平凡形式的并发性和分布;它们被期望在通信服务之间遵循预期的协议，但也永远不会“卡住”。这种直观的需求已经通过诸如进程或（死）锁自由的活动属性来表达，并且各种类型的系统确保并发进程具有这些属性。不幸的是，很少有人知道这些类型系统和它们诱导的类型化进程类之间的精确关系。本文首次对保证无死锁的消息传递进程的不同类型系统进行了比较研究。我们比较了两类无死锁类型进程，这里记为L和K。类L因其规范性而突出：它是从线性逻辑命题作为会话类型的Curry-Howard解释中产生的。通过将会话类型编码为具有用法的Kobayashi线性类型而获得的类K包括在其他类型系统中不可类型化的进程。我们表明，L是严格包括在K，并确定精确的条件下，他们一致。我们还提供了两个保持类型的翻译过程在K到过程在L。
2021-09-06 cs.LO
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic
本文提出Actris 2.0，一种基于会话类型的分离逻辑，用于在混合并发范式下证明消息传递程序的功能正确性，并通过子协议增强异步推理，已在Coq中机械化验证。
2022-06-08 cs.LO cs.PL
On the Impact of the Communication Model on Realisability
本文研究了不同通信模型对多方会话类型中可实现性的影响，提出统一框架并设计了不同复杂度的决策程序。
2025-12-05 cs.FL cs.LO
