Coherent differentiation
微分代数的范畴模型是加法范畴，因为莱布尼茨规则要求两个表达式求和。这意味着，就微分微积分和微分线性逻辑而言，这些模型具有有限的非确定性，实际上这些语言本质上是非确定性的。我们引入了一个分类框架分化，不需要添加剂，是兼容的确定性模型，如相干空间和概率模型，如概率相干空间。基于这种语义，我们勾勒出一个确定性的版本的差分dacalculus的语法。
2021-11-29 cs.LO
A categorical construction for the computational definition of vector spaces
Lambda-S是一阶λ演算的扩展，它统一了量子计算中的两种不可克隆方法。一种是禁止变量重复，而另一种是考虑所有的代数线性函数的代数项。Lambda-S的类型系统有一个构造函数S，使得类型A被认为是向量空间的基，而S（A）是它的跨度。Lambda-S也可以被看作是一种用于向量空间的计算操作的语言：向量空间公理作为重写系统给出，描述要执行的计算步骤。本文给出了Lambda-S*（Lambda-S的一个片段）的抽象范畴语义，证明了S可以解释为笛卡尔范畴和加法对称monoidal范畴之间的一个连接关系中两个函子的合成.右伴随是一个遗忘函子U，它隐藏在语言中，在计算推理中起着核心作用。
2020-04-11 cs.LO math.CT math.LO
On the Simply-Typed Functional Machine Calculus: Categorical Semantics and Strong Normalisation
本文研究函数机器演算（FMC）的范畴语义与强正规化，证明其在适当等式理论下对应自由笛卡尔闭范畴，并扩展 Gandy 证明以确立带类型 FMC 项的强正规化性质。
2023-05-25 cs.LO
Categorical E-Graphs for Lambda Calculi
University of Birmingham（伯明翰大学）；Kyoto University and Huawei Central Software Institute（京都大学和华为中央软件研究所）
针对 e-graphs 缺乏变量绑定支持的问题，本文基于范畴论框架扩展至闭对称幺半范畴，利用层次超图实现绑定，并提出双推重写机制，证明其与项重写的等价性。
2026-06-26 cs.LO math.CT
A Quick Overview on the Quantum Control Approach to the Lambda Calculus
在这个简短的概述中，我们从量子计算的基础知识开始，解释量子和经典控制范式之间的差异。我们给出了一个概述的量子控制线的研究范围内的λ演算，从无类型的演算到分类和realisability模型。这是对过去10多年来这一领域研究的总结，从Arrighi和Dowek的开创性工作开始直到今天。
2022-04-08 cs.LO
A Categorical Normalization Proof for the Modal Lambda-Calculus
本文为模态λ-演算提出基于Kripke式替换的求值归一化算法，证明其可靠完备，为元编程的依赖类型基础奠定逻辑基石。
2023-02-20 cs.LO cs.PL
A categorical framework for congruence of applicative bisimilarity in higher-order languages
本文提出一个范畴框架来规定操作语义，并证明其中应用双相似的抽象类比自动成为同余关系，涵盖按名调用、按值调用及非确定性λ演算等实例。
2022-09-20 cs.LO
Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus
本文从范畴和代数的角度研究了类型化λ演算的赋值正规化问题。本文的第一部分通过Kripke逻辑关系分析了Jung和Tiuryn的lambda可定义性结果，并展示了它如何适用于统一可定义性和规范化，产生一个扩展的规范化结果。在第二部分的文件的分析进一步细化考虑内涵Kripke关系（在阿丁胶合的形式），并显示提供一个功能的规范化条款，铸造规范化的范畴胶合的背景下进行评估。技术发展包括类型化λ演算的语法和语义的代数处理，其允许在简单类型化元理论内给出规范化函数的定义。合成依赖类型的函数式程序设计语言中的求值规范化程序。
2022-08-18 cs.LO math.CT
A coherent differential PCF
本文基于无需加性的范畴框架，开发了确定性版本的微分 lambda 演算语法，作为 PCF 的微分扩展并提供了完全确定性的操作语义。
2023-10-25 cs.LO
Syntactically and semantically regular languages of lambda-terms coincide through logical relations
本文证明简单类型λ-项的正则语言在语法（扩展Hillebrand-Kanellakis）与语义（有限外延模型）定义下等价，通过逻辑关系和胶合构造提供统一证明。
2024-02-08 cs.FL cs.LO cs.PL
Categorical Realizability for Non-symmetric Closed Structures
本文识别了产生闭多重范畴、闭范畴、幺半双闭范畴及非对称幺半闭范畴的平面应用结构类，建立了与平面lambda演算的严格对应，并引入平面线性组合代数，为非对称乘法直觉主义线性逻辑的线性指数模态和交换模态提供范畴模型。
2023-07-09 cs.LO
Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
本文概述了将Curry-Howard-Lambek对应扩展至量子计算的研究计划，通过提出Lambda-$S$演算和$\mathcal L^{\mathbb C}$演算两个框架，为量子编程语言建立逻辑与计算基础，揭示了量子计算与线性逻辑间的对偶性。
2025-04-10 cs.LO
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
University of Bath（巴斯大学）
本文提出利用热带几何工具对高阶概率程序进行统计推断，通过关联程序与度数和多面体，设计交类型系统以高效估计最可能运行。
2025-11-20 cs.LO
The dagger lambda calculus
我们提出了一种新的λ演算，将量子协议的分类方法引入到丰富而完善的类型论传统中。我们的构造扩展了线性类型的λ演算与线性否定的“trivialised”德摩根对偶。减少是通过明确的替代实现的，基于全局范围的绑定的对称概念，规则作用于整个类型判断，而不是特定的子项。证明的主题减少，汇合，强规范化和一致性，语言是一个内部语言匕首紧凑类。
2014-12-30 cs.LO cs.PL math.CT
Recovering Purity with Comonads and Capabilities
在本文中，我们采用了一种普遍有效的（ML风格的）类型λ演算，并展示了如何扩展它以允许捕获具有类型的纯表达式。我们的关键观察是，正如纯简单类型的λ演算可以扩展到支持一元类型规则的效果，不纯类型的λ演算可以扩展到支持一元类型规则的纯度。我们通过一个简单的指称模型来建立我们的类型系统的正确性，我们称之为能力空间模型。我们的模型形式化的直觉常见的系统程序员，执行效果的能力应该通过访问权限或能力进行控制，一个程序是能力安全的，如果它没有执行效果，它没有一个运行时的能力。然后，我们确定的公理范畴结构的能力空间模型验证，并使用这些公理给我们的comonadic类型系统的范畴语义。然后，我们给出了一个等式理论（替代和调用的值$β$和$η$法律）的命令λ演算，并显示其可靠性相对于此语义。最后，我们给出了一个翻译的纯简单类型的λ演算到我们的共同命令演算，并表明，任何两个条款是$βη$ -平等的STLC是平等的共同命令演算的方程理论，建立纯程序可以映射到我们的命令演算在一个方程保持的方式。
2020-11-10 cs.LO cs.PL
Higher-order semantics for quantum programming languages with classical control
本论文以类型论为理论框架，分三个层次研究量子计算的范畴形式化。我们研究的第一阶段涉及匕首λ演算的创建，匕首紧范畴的λ演算。我们的第二个贡献提升了表达能力的匕首λ演算，量子程序设计语言，通过添加经典控制的形式互补的经典结构和dualisers。最后，我们的第三个贡献演示了如何我们的λ演算可以应用到各种众所周知的量子计算问题。
2013-11-26 cs.LO cs.PL math.CT
A concrete model for a typed linear algebraic lambda calculus
本文为带测量的类型化线性代数 lambda 演算 Lambda-S 构造了基于集合与复向量空间范畴伴随关系的具体模型，用隐藏的遗忘函子解释叠加类型 S。
2023-10-11 cs.LO math.LO
Quantalic lambda-calculus and additive disjunction
University of Minho（米尼奥大学）；INESC-TEC；Forschungszentrum Jülich（于利希研究中心）
本文将量化线性 lambda 演算扩展为含加性析取的系统，证明其可靠性与近似完备性，给出多类模型并结合 Banach 空间概率模型实现随机游走柯西序列的量化推理，推动程序语义向量化视角转变。
2026-08-07 cs.LO math.CT
Strategies as Resource Terms, and their Categorical Semantics
ENS de Lyon（里昂高等师范学校）；Université Claude Bernard Lyon 1（里昂第一大学）；Aix Marseille Univ（艾克斯-马赛大学）
本文用增广因果结构直接刻画正规资源项与 Hyland-Ong 博弈的对应，并构造归约不变的资源演算指称模型及资源范畴。
2025-10-15 cs.LO
From Differential Linear Logic to Coherent Differentiation
本综述统一介绍相干微分的范畴与句法框架，提出通过可和性概念限制导数求和，解决微分线性逻辑与微分λ演算因莱布尼茨法则带来的非确定性问题，证明其与确定性相容。
2024-01-26 cs.LO
On the discriminating power of tests in resource lambda-calculus
自发现以来，差分线性逻辑（DLL）启发了许多领域。在指称语义中，DLL的范畴模型已经比较普遍，其中最简单的是Rel，即集合和关系的范畴。在证明论中，这自然产生了完全和完整的DLL差分证明网。反过来，这些工具可以自然地转化为它们的直觉对应物。通过采取共同克莱斯利类别相关联的！comonad，Rel变成MRel，一个包含微分概念的\Lcalcul模型。证明网可以很自然地用于将\Lcalcul扩展为具有资源的λ演算，一种包含线性和微分概念的演算。当然，MRel是一个有资源的\Lcalcul模型，它已经被证明是足够的，但是它是完全抽象的吗？这是布恰雷利、卡拉罗、埃哈德和曼佐内托的一个强有力的猜想。然而，在本文中，我们展示了一个反例。此外，为了更直观地了解反例的本质并寻求更大的普遍性，我们将使用Bucciarelli等人也引入的资源\Lcalcul的扩展，其中$\Minf$是完全抽象的，即测试。
2012-05-22 cs.LO cs.PL
On Geometry of Interaction for Polarized Linear Logic
我们提出了乘法极化线性逻辑（MLLP）的交互几何（GoI）模型，MLLP是Olivier Laurent的极化线性逻辑的乘法片段。这是通过将多个点均匀地添加到GoI的各种分类模型来完成的。在极化证明理论中，多点在语义上表征证明网络的动态性方面发挥着重要作用。例如，它们允许我们描述极化的关键特征，聚焦，以及我们构建具体极化GoI模型的基础。我们的方法两极分化GoI涉及两个独立的研究，根据不同的分类角度的GoI。(i)受Abramsky，Haghverdi和Scott工作的启发，定义了一个极化的GoI情况，其中多点被添加到配备有自反对象$U$的跟踪monoidal类别。使用这个框架，吉拉德的执行公式的分类版本的定义，以及GOI解释MLLP，证明。运行的执行公式示出的特征的聚焦属性（从而极性），以及动态的削减消除。(ii)Joyal-Street-Verity的Int构造是GoI建模的另一个基本范畴结构。在这里，我们调查它在一个多点设置。我们的演示文稿产生了一个紧凑的版本Hamano-Scott的极化类别，从而指称模型MLLP。这些产生于正和负对象的monoidal范畴之间的逆变对偶性，以及它们之间的适当双模结构（代表“非聚焦证明”）。最后，作为上述（ii）的一个特殊情况下，MLLP的紧凑模型也提出了基于Rel（集合和关系的范畴）配备了多点。
2017-04-07 cs.LO
A General Probabilistic Framework in IMALL: A Concrete Categorical Perspective
本文在交换半环上的半模范畴框架下研究量子计算背景下提出的sup类型构造子，证明非确定性析构子可由加权余对角映射建模，为幂集单子不适用的场景提供解释非确定性与概率演算的新方案。
2024-04-12 cs.LO math.CT math.LO
Formal P-Category Theory and Normalization by Evaluation in Rocq
本文在 Rocq 中形式化 P-范畴论，并据此证明纯范畴式 NbE 算法的可靠性与强完备性，支持提取计算 β-η-正规形及转换推导的程序。
2025-05-12 cs.LO math.CT
Profinite trees, through Lawvere theories and the lambda-calculus
Tallinn University of Technology（塔林理工大学）
本文通过 Lawvere 理论和 lambda-算子引入了克隆的 profinite 完成，从而为有限树的正则语言提供了一种拓扑方法，并证明了 profinite 树与 profinite lambda-算子的片段一致。
2026-02-09 cs.FL cs.LO math.CT
The Functional Machine Calculus II: Semantics
作者最近引入的函数机器演算（FMC）是拉姆达演算的推广，它可以忠实地编码高阶可变存储、I/O和概率/非确定性输入的影响。值得注意的是，它仍然是融合的，并且可以在这些效果存在的情况下简单地类型化。在本文中，我们探讨的指称语义的FMC。我们有三个主要的贡献：首先，我们认为，它的语法-在这两个效果，并实现使用相同的句法结构-是语义自然，密切对应的结构斯科特风格的域理论语义。第二，我们表明，简单的类型赋予强规范化扩展甘迪的证明，包括一个小的简化的技术。最后，我们表明，类型FMC（不考虑具体的编码效果），模适当的方程理论，是一个完整的语言笛卡尔闭范畴。
2023-02-05 cs.LO cs.PL
A theory of linear typings as flows on 3-valent graphs
建立在最近建立的枚举连接之间的λ演算和嵌入图（或“地图”）的理论，本文开发了一个类比之间的类型（λ条款）和着色（地图）。我们的出发点是抽象图上的阿贝尔群值“流”的经典概念（Tutte，1954）。输入一个线性lambda项可以被自然地看作是构造一个流（在一个嵌入的3-valve图上），该流在一个更一般的代数结构中取值，该代数结构由一个配备了“蕴涵”运算的预序集和满足组合、恒等式和单位定律的单位组成。流理论中有趣的问题和结果（例如无零流的存在）可以从λ演算和逻辑的观点重新审视。例如，我们给出了一个表征时，局部流关系（跨顶点）可以被分类提升到一个全局流关系（跨边界），证明这只是在情况下的底层地图有方向的lambda项。我们还开发了一个基本的理论重写的流，建议拓扑意义的经典完整性的结果组合逻辑，并介绍了一个极化的概念流，它绘制连接到理论的证明网络在线性逻辑和双向类型。
2018-04-27 cs.LO cs.PL math.CO
An Algebraic Extension of Intuitionistic Linear Logic: The $L_!^S$-Calculus and Its Categorical Model
Université de Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国国家信息与自动化研究所、洛林研究与信息学院）；Universidad Nacional de Quilmes, DCyT（基尔梅斯国立大学、计算机与信息技术系）；Universidad de Buenos Aires, DC, FCEyN（布宜诺斯艾利斯大学、计算系、经济与理学院）；Universidad de Buenos Aires-CONICET, ICC（布宜诺斯艾利斯大学-阿根廷国家科学研究委员会、计算中心）；Universidad de la República–MEC, PEDECIBA（共和国大学-教育部、PEDECIBA）；Universidad de la República, IMERL, FIng（共和国大学、IMERL、工程学院）
本文提出$L_!^S$-演算作为直觉线性逻辑的证明语言，通过标量乘法和项加法实现线性性的语法表达，并在范畴模型中提供语义解释。
2025-09-22 cs.LO math.CT
IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
Université Paris-Saclay（巴黎萨克雷大学）；CNRS（法国国家科学研究中心）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；Inria（法国国家数字技术研究所）；Laboratoire Méthodes Formelles（形式方法实验室）；Université de Lorraine（洛林大学）；LORIA（洛林信息与自动计算实验室）；Universidad Nacional de Quilmes（基尔梅斯国立大学）
本文提出一种扩展的IMALL证明语言，通过混合态模态B捕捉量子计算，支持线性组合和测量定义，并展示其在量子传送和量子开关中的应用。
2025-08-31 cs.LO
Cartesian Difference Categories: Extended Report
笛卡尔微分范畴是具有微分组合子的范畴，微分组合子公理化了方向导数。笛卡尔微分范畴的重要模型包括光滑函数的经典微分学和微分范畴的范畴模型。然而，笛卡尔微分范畴不能解释其他有趣的微分概念，如有限差分演算或布尔微分演算。另一方面，变革行动模式已被证明可以抓住这些例子以及更“奇特”的差异化例子。然而，变更行为模型非常通用，并且不具有笛卡尔微分范畴的良好特性。在本文中，我们引入笛卡尔差范畴之间的笛卡尔微分范畴和变化的行动模型的桥梁。我们表明，每一个笛卡尔微分范畴是一个笛卡尔差分范畴，以及如何某些行为良好的变化动作模型是笛卡尔差分范畴。特别是，笛卡尔差分范畴模型光滑函数的微分和有限差分的微积分。此外，每个笛卡尔差范畴都配备有切丛单子，其Kleisli范畴也是笛卡尔差范畴。
2020-07-22 cs.LO math.CT
Deductive Systems and Coherence for Skew Prounital Closed Categories
本文发展了斜原单位闭范畴的证明理论。这些都是街道的斜闭范畴的变体，其中单位不表示。反过来，斜闭范畴是艾伦伯格和凯利闭范畴的弱化，其中不需要结构律是可逆的。在这些类别中，不需要存在单体结构。我们构建了几个等价的表示的自由斜prounital闭范畴上一组给定的生成对象：一个范畴演算（希尔伯特式系统），一个切自由的代数演算和自然演绎系统对应的一个变体的平面（=非交换线性）类型的代数演算。我们解决了倾斜prounital封闭范畴的连贯性问题，通过显示，微积分承认聚焦和自然演绎演算提出两个约简自由规范化程序：通过评估和遗传替代规范化。正常的自然演绎推导（beta-eta-long形式）与集中式微积分中的推导一一对应。出乎意料的是，集合上的自由斜原单位闭范畴满足左正规性条件，这使得它失去了斜方面。通过考虑倾斜多类别上的自由倾斜原始封闭类别，可以避免这个陷阱。后者有一个演示文稿作为一个切自由的微积分，很容易看出，左正规性条件通常失败。整个开发已经完全形式化的依赖类型的程序设计语言Agda。
2021-01-11 cs.LO math.CT
