Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus
我们提出了一个形式化的会话类型在多线程λ演算（MTLC）配备了一个线性类型系统，建立MTLC类型保存和全球的进步。后者（全局进度）意味着在MTLC中对良好类型程序的评估永远不会陷入死锁。由于这个制定的MTLC可以很容易地嵌入到ATS，一个成熟的语言与功能的编程核心，支持依赖类型（的DML风格）和线性类型，我们得到了一个直接实现的会话类型在ATS。此外，我们获得了直接支持的依赖会话类型的基础上，这种嵌入到ATS的形式。与现有的各种会话类型的形式化相比，我们看到本文给出的形式化在其接近具体实现方面是独特的。特别是，我们报告这样一个实现准备实际使用，生成Erlang代码从良好类型的ATS源（利用会话类型），从而充分利用的基础设施支持分布式计算在Erlang。
2016-03-11 cs.LO cs.PL
Intersections and Unions of Session Types
先前的工作已经扩展了线性递归演算和会话类型的消息传递并发计算之间的深层逻辑联系，具有等递归类型和子类型的自然概念。在本文中，我们进一步扩展了交集和联合类型，以表示在一个单一的类型过程的多个行为属性。我们证明了会话的保真度和没有死锁，并说明了我们的系统的表达能力与一些简单的例子。我们观察到，我们可以表示内部和外部的选择的交集和工会，分别，这是以前建议由Padovani为不同的语言的会话类型的动机是操作，而不是逻辑问题。
2017-02-08 cs.LO cs.PL
Session Types with Arithmetic Refinements
会话类型静态地规定了消息传递过程的双向通信协议。但是，简单会话类型不能指定交换消息类型以外的属性。在本文中，我们通过使用线性算术的索引细化来扩展类型系统，捕获数据结构和算法的内在属性。我们发现，尽管Presburger算术的可判定性，类型平等，因此也子类型和类型检查现在是不可判定的，这与类似的依赖细化类型系统的函数语言。我们还提出了一个实用的，但不完整的算法类型的平等，我们已经在我们的实现Rast，并发会话类型的语言与算术索引的改进，以及测力和时间类型。此外，如果必要的话，程序员可以提出额外的类型互模拟，这些互模拟被平滑地集成到类型相等算法中。
2020-05-12 cs.LO cs.PL
Session Types as Generic Process Types
行为型系统比通常的静态分析更安全。它们基于“类型即进程”的思想，为特定的属性提供专用的类型代数，从协议兼容性到竞争自由、锁自由甚至响应性。有两种成功的方法，尽管它们有很大的不同，它们是会话类型和进程类型。前者允许使用特定类型（证明）系统来指定和验证（分布式）通信协议;后者允许从系统规范中推断出一个过程抽象，使用通用类型（证明）系统可以更简单地验证属性。这些方法之间的关系是什么？一般的一个可以substantially具体的一个？代价是什么？前者可以作为后者的编译器吗？本文介绍的工作是朝着回答这些问题迈出的一步。具体地说，我们定义了一个逐步编码的pi演算会话和会话类型（系统的盖伊和孔）到一个pi演算的进程类型（通用类型系统的五十岚和小林）。我们对会话类型环境、极性（区分会话通道端点）和标记总和进行编码。我们展示了编码的正向和反向操作对应，以及类型对应。为了在进程类型子类型中忠实地编码会话子类型，需要向目标语言添加记录构造函数和新的子类型规则。总之，作为协议抽象的会话类型的编程便利性可以与pi演算的简单性和功能相结合，特别是利用通用类型系统提供的框架。
2014-08-07 cs.LO cs.PL
Rast: A Language for Resource-Aware Session Types
Rast是一种开源语言，通过算术细化、ergometric/temporal类型和嵌套参数多态性扩展会话类型，以捕获并发程序的资源与复杂度属性，并借助优化后的Cooper算法进行类型检查。
2022-01-11 cs.LO cs.PL
Session Types with Runtime Adaptation: Overview and Examples
在最近的工作中，我们已经开发了一个会话类型的纪律演算，其特点是会话建立和通信的常用结构，但也有两个新的结构，使通信过程被停止，复制，或在运行时丢弃。目的是理解用于结构化通信的静态分析的已知技术是否可扩展到上下文感知的、可适应的分布式系统的具有挑战性的上下文，其中纪律化的交互和运行时适应是交织的关注点。在这篇简短的笔记中，我们总结了我们的会话类型框架的主要功能，并回顾了它的基本正确性属性。我们通过例子来说明我们的框架。特别是，我们提出了一个会话表示的监督树，执行容错应用程序的Erlang语言的机制。
2013-12-10 cs.LO cs.PL
Deconfined Global Types for Asynchronous Sessions
本文提出一种改进的异步多参与者会话类型系统，在满足良构条件时保留主体归约、会话保真和进展性质，并配有健全完备的类型推断算法，通过检查良构条件的受限形式恢复类型化的有效性。
2023-01-12 cs.LO cs.PL
Session Type Systems based on Linear Logic: Classical versus Intuitionistic
会话类型系统已经通过基于直觉和经典线性逻辑的Curry-Howard对应给出了逻辑基础。从这两个逻辑派生的类型系统在同一类的pi演算进程上强制通信正确性，但它们是显著不同的。Caires，Pfenning和Toninho非正式地观察到，与经典类型系统不同，直觉类型系统强制共享通道的局部性，即接收的通道不能用于复制输入。在本文中，我们从形式的角度重新审视这一观察。我们开发了统一线性逻辑（UnitedLinearLogic），一种包含经典线性逻辑和直觉线性逻辑的逻辑。然后，根据Curry-Howard对应的会话类型，我们定义了piectin，一个基于π演算的会话类型系统。使用pixel，我们可以正式评估直觉和经典类型系统之间的差异，并证明局部性和对称性在其中的作用。
2020-04-03 cs.LO cs.PL
Session Fidelity for ElixirST: A Session-Based Type System for Elixir Modules
本文建立在以前的工作调查的会话类型的适应提供有关Elixir模块的行为信息。一个名为ElixirST的类型系统已经被构建，用于静态确定Elixir模块中的函数是否遵守其端点规范，表示为会话类型;还构建了相应的自动化类型检查的工具。在本文中，我们正式验证这种类型的系统。一个基于LTS的操作语义的类型系统所支持的语言片段的开发，建模其运行时的行为时，调用的模块客户端。然后使用该操作语义来证明ElixirST的会话保真度。
2022-08-09 cs.LO cs.PL cs.SE
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
作为会话的命题（Propositions-as-Sessions）的出现，为消息传递并发奠定了逻辑基础，它是线性逻辑命题与并发进程会话类型之间的Curry-Howard对应。这种方法的核心是由线性逻辑预示的资源消耗范式。在本文中，我们研究了一个新的点，在设计空间的会话类型系统的消息传递并发程序。我们确定O 'Hearn和Pym的逻辑束的影响（BI）作为一个富有成效的基础解释的逻辑作为一个并发程序设计语言。这导致了对非线性资源的处理，这与基于线性逻辑的现有方法完全不同。我们介绍了一个新的$π$ -演算会话，称为$π$ BI，其最显着的特点是一个构造称为产卵，它表达了新的形式的共享，诱导BI的结构原则。我们说明了$π$ BI的表现力，并奠定了其基本理论：类型保存，死锁自由和弱规范化的结果良好的类型化进程;一个操作上健全和完整的仿射$λ$ -演算的类型化编码;和一个非干扰的结果访问资源。
2022-09-12 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
Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs
引入了一个具有最小和最大不动点的无穷大一阶线性逻辑。为了确保切割消除，我们施加了一个有效性条件的无限导子。我们的演算的目的是相互定义的归纳和共归纳线性谓词的丰富签名的原因。在一个主要的案例研究中，我们用它来证明强的二进制会话类型的进程下的异步通信语义的进展属性。据我们所知，这是这个性质的第一个证明。
2021-03-07 cs.LO cs.PL
Linear Contextual Metaprogramming and Session Types
本文研究在按值调用线性 lambda 演算中集成元编程，并基于多层上下文模态类型理论扩展至会话类型，支持代码装箱、传输、拆箱与本地按需运行。
2024-04-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
Mixed Choice Multiparty Session Types, Precisely
University of Oxford（牛津大学）
本文针对含会话委托等特性的混合选择多方会话类型，证明其子类型关系的精确性，开发通用类型系统并实现相关检查算法，经案例研究验证其有效性。
2026-08-12 cs.LO cs.PL
Higher-order Context-free Session Types in System F
我们提出了一个扩展的系统F与高阶上下文无关的会话类型。功能类型与会话类型的混合已经被证明是类型等价形式化的一个挑战：而功能类型等价通常是基于规则的，会话类型等价通常遵循基于互模拟的语义方法。我们提出了一个统一的方法，处理功能和会话类型的等价性在一起。我们提出了三个概念的类型等价：基于语法规则的版本，语义bisimulation-based版本，和算法版本减少到简单的语法的互模拟的问题。我们证明了这三个概念相吻合，并得出一个可判定性结果的类型等价问题的高阶上下文无关的会话类型。
2022-03-24 cs.FL cs.LO cs.PL
Recursive Session Logical Relations
程序等价是程序性质推理和证明的支点。对于不干扰，例如，程序等价的保密水平的观察员。逻辑关系是这种证明的有力推动者。逻辑关系直到最近才被用于会话类型--但仅用于终止语言。本文将逻辑关系扩展到递归会话类型。它为线性会话类型的进度敏感非干扰开发了一个逻辑关系，解决了非终止和并发带来的挑战。这些贡献包括安全多态过程和与元理论的逻辑关系。一个显着的特点是选择的“步骤指数”的逻辑关系，允许传递性和可靠性的自然证明。
2022-08-30 cs.LO cs.PL
Session Types with Arithmetic Refinements and Their Application to Work Analysis
会话类型静态地规定了消息传递过程的双向通信协议，并且与线性逻辑命题处于Curry-Howard对应关系中。但是，简单会话类型不能指定交换消息类型以外的属性。在本文中，我们扩展了类型系统，通过使用索引细化从线性算术捕捉内在属性的数据结构和算法，使我们可以表示和验证摊销成本的程序使用测力类型。我们发现，尽管Presburger算术的可判定性，类型平等，因此也类型检查现在是不可判定的，这与类似的依赖细化类型系统的函数语言。我们还提出了一个实用的不完全算法的类型相等和算法的类型检查，这是完整的相对于一个预言的类型相等。在这个显式语言的过程表达式是相当冗长的，所以我们也引入了一个隐式的形式和一个健全的和完整的算法重建显式程序，借用的想法，从证明理论的技术聚焦。最后，我们用各种例子说明了我们的系统和算法，这些例子在我们的实现中得到了验证。
2020-01-23 cs.LO cs.PL
A Logical Account of Subtyping for Session Types
本文在带不动点的线性逻辑框架下研究会话类型的子类型关系，提出一种同时保持安全性与终止性的子类型刻画，并证明该子类型在理论上可通过强制语义编译消除。
2023-04-13 cs.DC cs.LO cs.PL
Towards deductive verification of MPI programs against session types
消息传递接口（MPI）是开发并行应用程序的事实标准消息传递基础设施。在第一版库规范发布20年后，基于MPI的应用程序现在通常部署在超级计算机和集群计算机上。这些用C或Fortran编写的应用程序表现出复杂的消息传递行为，因此很难静态验证重要属性，例如不存在死锁。我们的工作建立在会话类型，一个理论描述协议，在这方面提供正确的建设保证。我们注释MPI原语和C代码与会话类型的合同，写在语言的软件验证C。然后用软件验证器检查带注释的代码的正确性。我们提出了初步的结果，并讨论了未来的挑战，验证现实的MPI程序符合会话类型。
2013-12-10 cs.DC cs.LO cs.PL
Affine Sessions
本研究将会话类型的线性性放宽为仿射性，允许通道最多执行规定行为，从而引入优雅的错误处理机制，并保持会话不卡住的进展属性。
2018-11-14 cs.LO cs.PL
The Different Shades of Infinite Session Types
许多类型系统包含无限类型。在会话类型系统中，这是本文的重点，无限类型是很重要的，因为它们允许通信协议的规范，是无限的时间。通常无限会话类型作为简单的有限状态表达式$\mathsf{rec}\, X.T$或通过非参数方程定义$X\doteq T$引入。或者，某些依赖于标签或值的会话类型系统超越了简单的递归类型。然而，撇开依赖类型不谈，无限会话类型的世界要丰富得多，从各种形式的参数方程定义，一直到共归纳定义空间中的任意无限类型。我们研究无限会话类型跨越灰色阴影的光谱的方式，一般无限类型的明亮的光。我们确定了四个点上的频谱，其特征在于不同风格的方程定义，并表明，他们形成了一个严格的层次结构，通过建立双向对应类的自动机：有限状态，1-计数器，下推和2-计数器。这使我们能够建立可判定性和不可判定性的结果的问题的类型形成，类型等价和对偶的每一类类型。我们还考虑了上下文无关会话类型（并将其扩展到高阶）和嵌套会话类型的先前工作，并将它们定位在我们的无限类型谱中。
2022-01-20 cs.FL cs.LO cs.PL
Session Type State Spaces Form Lattices
Independent Researcher, Berlin, Germany
本研究证明良构会话类型的状态空间经强连通分量商化后构成有界格，推导得到对偶性与子类型的格理论对应关系，并在108个基准协议上完成验证，同时实现了Lean 4机械化证明。
2026-09-28 cs.LO cs.PL
Session Types in Abelian Logic
有一个博士生说：“我找到了一双木鞋。我在左边放了一枚硬币，在右边放了一把钥匙。第二天早上，我在另一只鞋里发现了这些东西。“我们并不声称存在这样的鞋子，但在类型化lambda演算的上下文中提出了类似的编程抽象。我们称之为Amida演算的结果推广了Abramsky的线性λ演算LF并刻画了Abel逻辑.
2013-12-10 cs.LO cs.PL
A Gentle Overview of Asynchronous Session-based Concurrency: Deadlock Freedom by Typing
本文综述基于会话的异步并发领域研究，介绍三种带类型进程框架，阐述其如何为循环进程网络中异步通信的消息传递进程及带会话的并发函数式语言保障无死锁特性。
2024-12-11 cs.LO cs.PL
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
这项工作利用会话类型的逻辑基础，以确定什么样的类型纪律的π演算可以准确地捕获，并被捕获，π演算的行为。利用证明理论的内容的可靠性和完整性的微积分和自然演绎呈现的线性逻辑，我们开发了第一个相互逆和完全抽象的进程作为函数和函数作为进程编码之间的多态会话π演算和系统F的线性制定。然后，我们能够从会话演算的理论推导出会话演算的结果：（1）我们通过系统F中的代数表示获得归纳和共归纳会话类型的特征;（2）我们将结果扩展到值和进程传递，需要强规范化。
2018-01-25 cs.LO cs.PL
On the Fair Termination of Client-Server Sessions
客户-服务器的【形】会话基于线性逻辑命题作为会话类型的传统解释的变体，其中非线性通道（调节客户端池和单个服务器之间的交互的通道）由共指数而不是通常的指数来类型化。共指数能够对竞争交互进行建模，从而客户端竞争与单个服务器进行交互，该服务器的内部状态（以及所提供的服务）可能会随着服务器顺序处理请求而发生变化。在这项工作中，我们提出了一个公平的终止结果CSLL $^\infty$，客户-服务器的【形】会话的核心演算。我们设计了一个类型系统，使得每个类型良好的术语对应于$μ$ MALL $^\infty$中的一个有效推导，$^\infty$是线性逻辑的最小和最大不动点的无穷证明理论。然后，我们建立了一个对应关系之间的减少在微积分和主要减少在$μ$ MALL $^\infty$。CSLL $^\infty$中的公平终止来自$μ$ MALL $^\infty$中的切割消除。
2022-12-11 cs.LO cs.PL
Circular Proofs as Session-Typed Processes: A Local Validity Condition
本文扩展了直觉主义线性逻辑与会话类型π演算的对应关系到带最小和最大不动点的子结构逻辑片段，提出一个局部且可判定的有效性准则来识别对应有效循环证明的互递归进程，并证明该准则比既有守护条件更严格但更适合作编程语言基础。
2022-05-09 cs.LO cs.PL
Reversible Sessions Using Monitors
许多研究已经研究了正确和可靠的通信中心系统的基础。一个突出的正确性方法使用会话类型来强制结构化通信;最近的可靠性方法使用可逆动作作为对意外事件或故障的反应方式。本文提出了一个简单的观察：定义异步语义和监控所需的机制也可以支持可逆协议。我们提出了一个会话通信的过程框架，其中监视器支持可逆性。在我们的方法中，一个关键的新颖性是现在和过去的会话类型，这使我们能够简化可逆动作的语义。
2016-06-20 cs.LO 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
Subtyping on Nested Polymorphic Session Types
子类型对于支持更广泛的良好类型程序的重要性是不可否认的。然而，子类型、递归和多态之间的相互作用还没有完全理解。在这项工作中，我们探讨子类型的嵌套，递归和多态类型的系统与共归纳的解释，我们证明了这个问题是不可判定的。我们的结果将是广泛适用的，但保持我们的研究扎根在一个具体的设置，我们的工作与显式多态性，参数类型构造函数，嵌套类型的会话类型的扩展。我们证明了子类型是不可判定的，即使是只有内部选择和嵌套的一元递归类型构造函数的片段。尽管这个负面的结果，我们提出了一个子类型算法，我们的系统，并证明其可靠性。我们通过使程序员能够用子类型声明（由算法验证）来播种算法，从而最大限度地减少不可避免的不完整性的影响。我们已经在Rast中实现了该算法，并在各种示例程序中证明了其有效性。
2021-03-28 cs.LO cs.PL
Timed Session Types
本文提出定时会话类型的合规判定与最精确合规类型构造技术，并由此证明子类型可判定性。
2017-12-07 cs.LO
Probabilistic Analysis of Binary Sessions
我们研究了一个概率变量的二进制会话类型，涉及到一类随机状态马尔可夫链。会话类型中的概率注释使得能够对会话成功终止的概率进行推理，对于某些用户可定义的成功终止概念。我们开发了一个简单的会话演算具有概率选择的类型系统，并表明良好类型的进程的成功概率与他们使用的会话。为此，类型系统需要跟踪概率选择在不同会话中的传播。
2020-07-23 cs.LO
Partially Typed Multiparty Sessions
针对标准类型系统无法为部分含可忽略通信的多方会话做类型标注的问题，提出满足主体归约、会话保真度与部分无锁性的类型系统，并给出可靠完备的类型推断算法。
2023-08-21 cs.LO
Client-Server Sessions in Linear Logic
我们介绍了共指数，一组新的模态经典线性逻辑。作为一种非线性指数，共指数将弱化和收缩的结构规则编成了一种分布形式。这使得它们成为一种合适的逻辑设备，用于封装服务器在单个通道上接收来自任意数量客户端的请求的模式。在这种直觉的指导下，我们制定了一个系统的会话类型的基础上，经典的线性逻辑与coexponentials，这是适合于客户-服务器的【形】交互建模。我们还提出了一个会话类型的功能程序设计语言的服务器-客户端编程，我们翻译到我们的系统的共指数。
2021-03-03 cs.LO cs.PL
Global types and event structure semantics for asynchronous multiparty sessions
INRIA（法国国家信息与自动化研究所）；Université Côte d’Azur（蔚蓝海岸大学）；Dipartimento di Informatica Università di Torino（都灵大学计算机系）；Università del Piemonte Orientale（皮埃蒙特东方大学）
本文提出将异步通信的多方会话解释为流事件结构，并引入新的全局类型概念，确保会话的预期属性，如进展。全局类型通过更直接地反映异步性并更宽松地解释为原始事件结构。
2024-07-16 cs.LO
Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom
我们研究不同的公平性假设如何影响锁自由，一个典型的会话类型系统的活性属性为目标的结果。我们修复了一个最小的会话演算，并系统地考虑到所有已知的公平性假设，从而准确地确定三个有趣的和语义上不同的概念锁自由，所有这些都有一个健全的会话类型系统。然后，我们表明，通过使用一个通用的合并运算符，否则标准的方法来全局会话类型，我们得到一个会话类型系统完成最强的锁自由的概念，它只假设公正的执行路径，最小的公平性假设并发系统。
2021-04-29 cs.LO
On Urgency in Asynchronous Timed Session Types
我们研究了异步定时会话类型的紧急语义，其中输入动作尽快发生。我们表明，这种语义，我们可以恢复到定时设置一个有吸引力的属性不定时的会话类型：即，死锁自由时，保持从同步到异步通信。
2018-10-05 cs.LO
Session Types for Link Failures (Technical Report)
我们努力使用会话类型技术来证明容错分布式算法的行为特性。会话类型被设计为抽象地捕获（甚至多方）通信协议的结构。会话类型的目标是分析和验证协议的行为属性。一个重要的属性是进步，即，没有（意外的）死锁。分布式算法通常类似于多方通信协议（的组合）。与通常研究会话类型的协议相反，它们通常被设计为应对系统故障。一个基本的行为属性是（成功）终止，尽管失败，但它往往是精心证明分布式算法。我们通过可选块扩展了多方会话类型（以及具有嵌套会话的多方会话类型），这些可选块覆盖了有限的链接和崩溃故障类。这使我们能够自动推导出在这些限制范围内的分布式算法的终止。为了说明我们的方法，我们证明终止的 * 旋转协调 * 共识算法的实施。
2017-05-04 cs.LO
Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols
组合方法是软件系统开发和验证的核心。它们允许将大型系统分解为较小的组件，同时支持对组合系统的行为进行推理。对于并发和通信系统，基于行为类型系统的组合技术受到了广泛的关注。通过将通信协议抽象为类型，这些类型系统可以静态地检查程序是否根据某个协议与通道交互，以及预期的消息是否以某个顺序交换。在本文中，我们把我们的coalgebraic眼镜调查会话类型，一类广泛研究的行为类型系统。我们提供了一个无语法的描述会话为基础的并发状态的余代数。其结果是，我们重新发现类型等价，对偶，和子类型的关系，在规范的共归纳介绍。反过来，这coinductive介绍，使人们有可能优雅地得出一个可判定的类型系统与子类型的$π$演算过程，其中的状态的一个coalgebra将作为信道协议。走一圈，我们展示了一个现有的会话类型系统的余代数结构，并表明，从我们的余代数的角度来看，关系和类型系统与现有的。
2020-11-11 cs.LO
Characteristic Formulae for Session Types (extended version)
子类型是会话类型论及其应用的关键组成部分，特别是在程序设计语言实现中。在本文中，我们研究了有效的方法来检查是否一个会话类型是另一个的子类型，通过应用特征公式的方法来解决这个问题。我们的核心贡献是一个算法来生成一个模态μ演算公式，该公式描述了给定类型的所有超类型（或子类型）。然后，子类型检查可以卸载到模型检查器，从而附带地产生一个有效的算法来检查会话类型的安全性，可靠而完整。我们已经实现了我们的理论，并比较其成本与其他经典的子类型算法。
2015-10-23 cs.LO
Open Multiparty Sessions
多方会话是并发进程的系统，它允许多个参与者通过发送和接收消息进行通信。它们的整体行为可以通过全局类型来描述。可键入的多方会话享受锁自由。我们把多方会话看作是一个开放系统，通过一个合适的连接定义将兼容的进程转换为网关（转发器）。类似于会话类型的标准子类型关系的关系用于形式化兼容性。我们表明，通过连接获得的会话可以通过操纵启动会话的全局类型进行类型化。这使我们能够证明锁自由被连接保持。
2019-09-12 cs.LO
Linearly Refined Session Types
在并发编程中，会话类型捕获精确的协议结构，但不指定交换值的基本类型之外的属性。细化类型是一种依赖类型，可以解决这种限制，将类型与可能引用程序值的逻辑公式组合，并可以使用任意谓词约束类型。我们提出了一个PI演算的假设和断言操作，使用会话的纪律，结合细化公式写在一个片段的乘法线性逻辑。我们原来的会话和细化类型的组合，以及良好的线性的好处，允许非常细粒度的通信协议规范，其中细化公式被视为逻辑资源，而不是持久的真理。
2012-11-17 cs.LO
Session Types for Orchestrated Interactions
在设置的π演算与二进制会话，我们的目标是放松的概念，会话类型的对偶性的概念，可伸缩的遵守合同理论。这导致使用“推测选择”的新类型操作符扩展会话类型，包括不一定由兼容伙伴提供的选择。我们解决的问题，选择成功的通信分支机构的操作语义的基础上orchestration，这已被证明是等同于合同的可伸缩语义，但显然更可行。因此，提供了一种类型系统，相对于这样的语义是合理的。
2017-11-30 cs.LO
Probabilities in Session Types
本文讨论了分布式系统的概率行为描述的过程演算考虑概率的内部选择和非确定性的外部选择。对于这个演算，我们定义和研究的类型系统，扩展了多方会话类型，以处理概率行为。通过一个运行的例子，对演算及其类型化系统进行了说明.
2019-09-04 cs.LO
System $F^μ_ω$ with Context-free Session Types
我们研究越来越多的表达类型系统，从$F^μ$ --多态lambda演算的等递归类型的扩展--到$F^{μ;}_ω$ --高阶多态λ演算的等递归类型和上下文无关的会话类型。类型等价由定义在一个新的类型标记转换系统上的标准互模拟给出。我们的系统包含了文献中研究的$F^μ_ω$的收缩片段。各种类型语言的类型等价的可判定性结果是通过将类型转换为适当的计算模型的对象来获得的：有限状态自动机、简单语法和确定性下推自动机。我们表明，类型等价是可判定的类型语言的一个重要片段。我们进一步提出了一个消息传递，并发函数语言配备了表达类型语言，并表明它享有保存和不存在的运行时错误的类型化进程。
2023-01-20 cs.FL cs.LO cs.PL
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
Event structure semantics for multiparty sessions
我们提出了一个多方会话的解释为“流事件结构”，它允许在一个会话内的通信之间的并发被明确表示。我们表明，这种解释是等价的，当多方会话可以描述的全球类型，全球类型的“总理事件结构”的解释。
2022-05-17 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
Using higher-order contracts to model session types
会话类型用于描述和构造分布式系统中独立进程之间的交互。为了正确地构造进程之间的责任委托，需要更高阶的类型。在本文中，我们表明，高阶Web服务合同可以用来提供一个完全抽象的递归高阶会话类型的模型。该模型是集合论的，在这个意义上，一个合同的意义是根据它所遵守的一组合同来给出的。完全抽象的证明依赖于一个新的契约补集的概念。这反过来又产生了一个替代的类型二重性通常用于系统中的类型检查会话类型。我们相信，补语的概念更忠实地抓住了类型二元性背后的行为直觉。
2016-06-28 cs.LO
Asynchronous Multiparty Sessions with Mixed Choice
Università di Catania（卡塔尼亚大学）；Università di Torino（都灵大学）
本文提出一种异步多方会话的校验算法，支持输入和输出前缀的非确定性选择，通过全局类型系统确保通信标签集的连贯性，证明了类型正确性和会话保真性，展示了混合选择在异步多方协议中的表达力。
2026-04-08 cs.LO
Partial Typing for Asynchronous Multiparty Sessions
本文针对并发系统验证难以局部化的问题，提出异步多方会话的部分类型指派系统，并证明其可类型性保证部分锁自由与孤儿消息自由。
2024-10-01 cs.LO
A Session Type System for Asynchronous Unreliable Broadcast Communication
本文提出不可靠广播会话演算及其会话类型系统，刻画广播与汇聚的对偶会话类型，并提供无需确认的自主恢复机制，通过实现Paxos协议验证了框架的表达能力。
2024-08-02 cs.FL cs.LO
Parameterised Multiparty Session Types
对于许多应用级分布式协议和并行算法，参与者的集合、消息的数量或交互结构仅在运行时才知道。本文提出了一个多方会话的依赖类型论，它可以静态地保证类型安全的，无死锁的多方进程之间的互动，其规格由索引参数化。我们使用哥德尔系统T中的原始递归运算符来表达广泛的通信模式，同时保持类型检查的可判定性。为了对单个分布式进程进行类型化，将参数化的全局类型投影到表示所有可能的端点类型的类的通用生成器上。我们证明了终止的类型检查算法在整个系统与多方会话类型和递归类型。我们说明了我们的类型论通过非平凡的编程和验证的例子，从并行算法和Web服务用例。
2012-10-10 cs.LO
