功能作为证明作为过程

循环证明作为会话类型进程：一种局部有效性条件

Circular Proofs as Session-Typed Processes: A Local Validity Condition

本文扩展了直觉主义线性逻辑与会话类型π演算的对应关系到带最小和最大不动点的子结构逻辑片段，提出一个局部且可判定的有效性准则来识别对应有效循环证明的互递归进程，并证明该准则比既有守护条件更严格但更适合作编程语言基础。

PiL的证明网络（完整版本）

Proof Nets for PiL (Full Version)

本文提出PiL的证明网络，扩展了第一阶乘积加法线性逻辑，引入新运算以浅层编码π演算过程。提供正确性准则、序列化过程及证明翻译算法，展示证明网络是序列演算推导的规范表示。

关于二阶下推过程双相似不可判定性的注记

Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes

Broadbent和Göller（FSTTCS 2012）证明了无ε二阶下推自动机生成的过程的互模拟等价性的不可判定性。我们添加了一些关于所使用的证明技术的注释，称为Defender's forcing，以及具有ε转换的一阶下推自动机的相关不可判定性证明（Jančar and Srba，JACM 2008）。

直觉幺正线性逻辑：纯量子高阶的证明论方法

Intuitionistic Unitary Linear Logic: A Proof-Theoretical Approach to Purely Quantum Higher-Order

本文针对线路模型无法表示非因果高阶量子过程的问题，提出基于柯里-霍华德对应的直觉幺正线性逻辑（IULL），证明其一致性、完备性及割规则可容许性，通过实例验证了方法的有效性。

具有双积的紧范畴的广义证明网

Generalised Proof-Nets for Compact Categories with Biproducts

正如传统的函数程序可以被理解为直觉主义逻辑中的证明一样，量子过程也可以被视为合适逻辑中的证明。我们描述这样一个逻辑，紧凑的闭范畴和biproducts的逻辑，提出了作为一个微积分和作为一个系统的证明网。这种逻辑捕捉了在经典控制下表示量子过程所需的大部分必要结构，同时对细节保持不可知论。我们演示了如何表示量子过程的证明网，并表明量子过程的动态行为被捕获的逻辑的削减消除过程。我们表明，削减消除程序是强烈规范化：也就是说，每一个法律的简化证明网络的方式导致相同的，唯一的，正常的形式。最后，采取一些初始的操作作为非逻辑公理，我们表明，由此产生的类别的证明网是一个表示的自由紧凑的闭范畴与这些操作所产生的双产品。

经典跃迁

Classical Transitions

我们介绍了演算的经典过渡（CT），它扩展了线性逻辑和过程之间的关系的研究线标记的过渡。从以前的工作中的关键转折是注册并行打字判断，通过概括线性逻辑判断从一个序列到许多（hypersequents）。这使我们能够弥合以前工作中用作证明项的算子结构与标准π演算（特别是并行算子和限制）之间的差距。CT的证明理论允许新的证明变换，我们显示对应于过程的标记转换系统（LTS）。我们证明了CT的学科减少和进步。

$\unicode{8523}$的意思是并行：乘法线性逻辑证明作为并发函数程序

$\unicode{8523}$ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

沿着Abramsky的“Proofs-as-Processes”程序的路线，我们提出了一个乘法线性逻辑作为并发函数编程的类型系统的解释。特别是，我们研究了线性多结论自然演绎系统，并表明它是同构的一个简单而自然的扩展$λ$ -演算的并行性和通信原语，称为$λ_{\unicode{8523}}$。我们将证明$λ_{\unicode{8523}}$满足类型化程序设计语言的所有理想属性：主题减少，进展，强规范化和汇合。

顺序算法与经典证明的计算内容

Sequential algorithms and the computational content of classical proofs

通过Kreisel的无反例解释，我们建立了顺序算法理论与经典推理之间的对应关系。我们的框架视图实现者的无反例解释的动态过程中与一个甲骨文，并允许这些过程在任何给定的抽象层次进行建模。我们讨论的一般结构的算法，代表特定的模式，经常出现在经典推理，特别是，我们开发了一个计算解释的规则，依赖选择的措辞纯粹的算法的水平，让我们更清楚地了解计算意义的证明在经典分析。

基于资源的过程组合

Correct by Construction Resource-based Process Composition

在涉及复杂系统的开发和分析的许多情况下，都需要严格的过程组合。我们讨论了使用经典线性逻辑（CLL）的正确的建设资源为基础的过程组合。抽象过程被指定为描述输入和输出资源类型的CLL序列。Proofs-as-Processes范式及其最近的发展使这些流程能够通过逻辑推理进行组合，并在并发执行、无死锁和系统资源核算方面提供数学保证。我们引入算法来自动化必要的推理步骤，并行，有条件和顺序的过程中的二进制组合物。我们结合决策程序和算法，以实现直观和实用的组合物中应用的设置。我们的工作是在HOL Light证明助手的正式设置中实现的，并被纳入WorkflowFM原型中，以促进图形化的、按施工纠正的流程工作流。

基本进程代数的双相似性在2- ExpTime中（一个显式证明）

Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)

Burkart，Caucal，Steffen（1995）给出了一个在基本进程代数（BPA）中确定进程互模拟等价的过程，即由上下文无关文法生成的顺序进程。他们改进了Christensen，Hüttel，Stirling（1992）先前的可判定性结果，因为他们的过程显然具有基本的时间复杂度，并且作者声称仔细分析会揭示双指数上界。这里给出了2-ExpTime中成员资格的自包含直接证明。这是通过一个证明反驳游戏，其中显示，有一个交替的图灵机决定指数空间中的问题。证明使用类似的成分（大小措施，分解，基地）作为以前的证明，但一个新的简化因素是一个明确的无限正规字符串添加到状态空间。辅助索赔也显示了显式指数上界的等价水平的nonbisilimited赋范BPA过程。由于已知的下限从PSpace（Srba，2002）转移到ExpTime（Kiefer，2012），澄清BPA双相似性的2-ExpTime上限的重要性最近有所增加。

An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $π$-Calculus

Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of $μ$MALL$^\infty$, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of $π$LIN, a variant of the linear $π$-calculus with (co)recursive types into which binary and (some) multiparty sessions can be e…

经典高阶过程

Classical Higher-Order Processes

经典过程（CP）是一种演算，其中经典线性逻辑类型的证明理论与移动通道通信过程，一个la pi演算。它的结构建立在最近的命题作为类型之间的会话类型和线性逻辑命题的对应关系。期望的属性，如在约简和进展下的类型保持，来自线性逻辑的元理论。我们有助于这一研究线扩展CP代码的流动性。我们概括了经典的线性逻辑，以捕捉高阶（线性）推理的证明，这产生了一个逻辑重建（变种）的高阶π演算（HOPI）。由此产生的演算被称为经典高阶过程（CHOP）。我们探讨CHOP的元理论，证明其语义享有类型保护和进步（条款不卡住）。我们还说明了CHOP的表现力，通过例子，派生的语法糖，并扩展到多方会议。最后，我们定义了一个从CHOP到CP的翻译，它将进程代码的移动性编码为引用传递。

基于概率耦合的关系推理

Relational reasoning via probabilistic coupling

概率耦合是分析概率过程对的有力工具。粗略地说，耦合两个过程需要找到一个合适的见证过程，在同一概率空间中对两个过程进行建模。耦合是证明两个过程之间关系的强大工具，包括关于分布收敛和随机优势的推理-单调性属性的概率版本。虽然耦合的数学定义看起来相当复杂和繁琐的操作，我们表明，关系程序逻辑pRHL-逻辑基础的EasyCrypt密码证明助手-已经内化的概率耦合的泛化。有了这种见解，构造耦合并不比构造逻辑证明难。我们演示了如何表达和验证pRHL耦合的经典例子，我们机械地验证了EasyCrypt中的几个耦合。

3D-Prover：基于行列式点过程的多样性驱动定理证明

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes

针对自动定理证明搜索空间过大的问题，提出3D-Prover方法，通过行列式点过程筛选语义多样的高质量证明策略，可增强各类证明LLM，在多个基准上提升了证明效率与成功率。

Synchronous Forwarders

Session types are types for specifying protocols that processes must follow when communicating with each other. Session types are in a propositions-as-types correspondence with linear logic. Previous work has shown that a multiparty session type, a generalisation of session types to protocols of two or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality. And, protocols expressed as coherence can be simulated by arbiters, processes that act as a middleware by forwarding messages according to the given protocol. In this paper, we generalise the concept…