Computational Adequacy for Substructural Lambda Calculi
子结构类型系统，例如仿射（和线性）类型系统，是对变量的复制（和丢弃）施加限制的类型系统，并且它们在计算机科学中有许多应用，包括量子编程。我们描述了一个线性和仿射型系统，我们制定了抽象的分类模型，它们都是健全的和计算足够的。我们还表明，在基本假设下，解释lambda抽象通过一个monoidal封闭结构（一种流行的方法，线性类型系统）必然导致退化和不足的模型调用值仿射型系统递归。在我们的分类处理中，清楚地提出了这个问题的解决方案。我们的分类模型比用于研究线性逻辑的线性/非线性模型更一般，并且我们在按值调用设置中提出了线性和仿射类型系统的齐次分类帐户。我们还给出了许多具体模型的例子，包括经典和量子模型。
2021-01-26 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 linear-non-linear model for a computational call-by-value lambda calculus (extended abstract)
给出了按值调用线性λ演算的范畴语义。这种λ演算被塞林格和Valiron用作量子计算的函数式程序设计语言的主干。这个λ演算的一个特性是它的线性类型系统，它包括一个可重复性操作符“！“就像线性逻辑一样另一个主要特性是它的按值调用减少策略，以及对概率测量建模的副作用。“！“运算符产生一个comonad，如Seely，Bierman和Benton的线性逻辑模型。副作用产生了单子，就像莫吉的计算λ演算。这是一个单子和一个comonad的组合，使本文件有趣。我们表明，我们的范畴语义是健全的和完整的。
2008-01-05 cs.LO
Coherent differentiation
微分代数的范畴模型是加法范畴，因为莱布尼茨规则要求两个表达式求和。这意味着，就微分微积分和微分线性逻辑而言，这些模型具有有限的非确定性，实际上这些语言本质上是非确定性的。我们引入了一个分类框架分化，不需要添加剂，是兼容的确定性模型，如相干空间和概率模型，如概率相干空间。基于这种语义，我们勾勒出一个确定性的版本的差分dacalculus的语法。
2021-11-29 cs.LO
Realizability in the Unitary Sphere
本文提出了一种基于可实现性的线性代数演算的语义。这种语义描述了系统中统一性的概念，回答了一个长期存在的问题。我们从语义中推导出一组简单类型的线性代数演算的类型规则，并展示了它如何扩展到经典和量子代数代数演算。
2019-04-18 cs.LO
On the Simply-Typed Functional Machine Calculus: Categorical Semantics and Strong Normalisation
本文研究函数机器演算（FMC）的范畴语义与强正规化，证明其在适当等式理论下对应自由笛卡尔闭范畴，并扩展 Gandy 证明以确立带类型 FMC 项的强正规化性质。
2023-05-25 cs.LO
A Categorical Normalization Proof for the Modal Lambda-Calculus
本文为模态λ-演算提出基于Kripke式替换的求值归一化算法，证明其可靠完备，为元编程的依赖类型基础奠定逻辑基石。
2023-02-20 cs.LO cs.PL
A Quick Overview on the Quantum Control Approach to the Lambda Calculus
在这个简短的概述中，我们从量子计算的基础知识开始，解释量子和经典控制范式之间的差异。我们给出了一个概述的量子控制线的研究范围内的λ演算，从无类型的演算到分类和realisability模型。这是对过去10多年来这一领域研究的总结，从Arrighi和Dowek的开创性工作开始直到今天。
2022-04-08 cs.LO
The dagger lambda calculus
我们提出了一种新的λ演算，将量子协议的分类方法引入到丰富而完善的类型论传统中。我们的构造扩展了线性类型的λ演算与线性否定的“trivialised”德摩根对偶。减少是通过明确的替代实现的，基于全局范围的绑定的对称概念，规则作用于整个类型判断，而不是特定的子项。证明的主题减少，汇合，强规范化和一致性，语言是一个内部语言匕首紧凑类。
2014-12-30 cs.LO cs.PL math.CT
Quantalic lambda-calculus and additive disjunction
University of Minho（米尼奥大学）；INESC-TEC；Forschungszentrum Jülich（于利希研究中心）
本文将量化线性 lambda 演算扩展为含加性析取的系统，证明其可靠性与近似完备性，给出多类模型并结合 Banach 空间概率模型实现随机游走柯西序列的量化推理，推动程序语义向量化视角转变。
2026-08-07 cs.LO math.CT
Higher-order semantics for quantum programming languages with classical control
本论文以类型论为理论框架，分三个层次研究量子计算的范畴形式化。我们研究的第一阶段涉及匕首λ演算的创建，匕首紧范畴的λ演算。我们的第二个贡献提升了表达能力的匕首λ演算，量子程序设计语言，通过添加经典控制的形式互补的经典结构和dualisers。最后，我们的第三个贡献演示了如何我们的λ演算可以应用到各种众所周知的量子计算问题。
2013-11-26 cs.LO cs.PL math.CT
A categorical framework for congruence of applicative bisimilarity in higher-order languages
本文提出一个范畴框架来规定操作语义，并证明其中应用双相似的抽象类比自动成为同余关系，涵盖按名调用、按值调用及非确定性λ演算等实例。
2022-09-20 cs.LO
On the Invariance of the Unitary Cost Model for Head Reduction (Long Version)
λ演算是一种被广泛接受的高阶函数程序的计算模型，但目前还没有一个直接的、普遍接受的代价模型，因此，将lambda项约简为其范式的计算难度通常是通过对具体实现算法的推理来研究的。在本文中，我们表明，当头部减少的基本动力学，单位成本模型确实是不变的。这改进了已知的结果，这些结果只处理弱（按值调用或按名称调用）约简。不变性是通过显式替换的线性演算来证明的，这允许很好地将λ演算中的任何头部减少步骤分解为更基本的替换步骤，从而使头部减少的组合学更容易推理。该技术也是一个很有前途的工具来攻击我们所看到的主要开放问题，即理解哪些规范化策略推导复杂性是不变成本模型（如果有的话）。
2012-02-08 cs.LO cs.PL
A coherent differential PCF
本文基于无需加性的范畴框架，开发了确定性版本的微分 lambda 演算语法，作为 PCF 的微分扩展并提供了完全确定性的操作语义。
2023-10-25 cs.LO
Abstract structure of unitary oracles for quantum algorithms
我们证明了一对互补的dagger-Frobenius代数，配备了一个自共轭同态到代数之一，产生一个非平凡的酉态射的产品的代数。这给出了一个抽象的理解，在量子计算中的神谕的结构，我们应用这种理解，开发一个新的算法，确定性识别群同态到阿贝尔群。我们还讨论了信号流网络的范畴理论的应用。
2014-12-30 cs.LO math.CT quant-ph
Fitch-Style Modal Lambda Calculi
Fitch风格的模态演绎，其中模态通过打开一个从属证明来消除，并通过关闭一个来引入，在20世纪90年代被研究作为lambda演算的基础。我们表明，这样的演算有良好的计算性能的各种直觉模态逻辑。语义是在配备了一个endofunctors的附加词的carnival封闭范畴中给出的，必要性模态由右伴随词解释。这个函子是一个幂等的comonad，语义上的一致性结果使我们能够提出一个演算的直觉S4比其他文献中的简单。我们证明了演算可以用必然性的左伴随扩展为时态逻辑，并且对于范畴语义是完备的。
2018-01-19 cs.LO
Recovering Purity with Comonads and Capabilities
在本文中，我们采用了一种普遍有效的（ML风格的）类型λ演算，并展示了如何扩展它以允许捕获具有类型的纯表达式。我们的关键观察是，正如纯简单类型的λ演算可以扩展到支持一元类型规则的效果，不纯类型的λ演算可以扩展到支持一元类型规则的纯度。我们通过一个简单的指称模型来建立我们的类型系统的正确性，我们称之为能力空间模型。我们的模型形式化的直觉常见的系统程序员，执行效果的能力应该通过访问权限或能力进行控制，一个程序是能力安全的，如果它没有执行效果，它没有一个运行时的能力。然后，我们确定的公理范畴结构的能力空间模型验证，并使用这些公理给我们的comonadic类型系统的范畴语义。然后，我们给出了一个等式理论（替代和调用的值$β$和$η$法律）的命令λ演算，并显示其可靠性相对于此语义。最后，我们给出了一个翻译的纯简单类型的λ演算到我们的共同命令演算，并表明，任何两个条款是$βη$ -平等的STLC是平等的共同命令演算的方程理论，建立纯程序可以映射到我们的命令演算在一个方程保持的方式。
2020-11-10 cs.LO cs.PL
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
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
A concrete model for a typed linear algebraic lambda calculus
本文为带测量的类型化线性代数 lambda 演算 Lambda-S 构造了基于集合与复向量空间范畴伴随关系的具体模型，用隐藏的遗忘函子解释叠加类型 S。
2023-10-11 cs.LO math.LO
The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics
本文的目的是提供数学基础的图形转换语言，称为UnCAL，使用类别语义的类型论和不动点。大约20年前，Buneman等人在函数元语言UnCAL之上开发了一种图形数据库查询语言UnQL，用于描述和操作图形。最近，函数式编程社区对UnCAL表现出了新的兴趣，因为它提供了一种有效的图形转换语言，可用于各种应用程序，如双向计算。为了使UnCAL更灵活和富有成效的进一步扩展和应用，在本文中，我们给出了一个更概念化的理解UnCAL使用范畴语义。本文的主要目的是弄清楚UnCAL的代数是什么。因此，我们给出了UnCAL的等式公理化和范畴语义，这两个都是新的。我们发现，公理化是完整的原始互模拟语义UnCAL。此外，我们提供了一个干净的特性的计算机制UnCAL称为“结构递归图”使用我们的分类语义。我们展示了一个具体的模型UnCAL给出的LiddaG演算，这表明了一个有趣的连接到懒惰的函数式编程。
2016-09-11 cs.DB cs.LO
String Diagrams for $λ$-calculi and Functional Computation
本教程以系统方式介绍高阶计算的字符串图与图语言，从范畴论概念的二维语法逐步深入到笛卡尔闭范畴，通过从范畴模型重构分层超图语法并探讨其在编程语言领域的应用。
2024-12-04 cs.LO cs.PL math.CT
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
本文提出利用热带几何工具对高阶概率程序进行统计推断，通过关联程序与度数和多面体，设计交类型系统以高效估计最可能运行。
2025-11-20 cs.LO
Course-of-Value Induction in Cedille
在分类设置中，组织态构建模了一个值过程递归方案，该方案允许使用任意先前计算的值来定义函数。在本文中，我们使用依赖λ消除（CDLE）的演算推导出一个归纳数据集，承认课程的价值归纳的λ-编码。类似于价值过程递归，价值过程归纳给出了在函数的归纳参数的任意深度处的归纳假设。通过证明Lambek引理和归纳原理的计算行为，我们证明了导出的价值过程数据集是良好的。我们的工作是正式的Cedille程序设计语言，还包括几个例子的课程的价值函数。
2019-03-07 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
Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism
本文在范畴论的框架内，通过对基于Curry-Howard同构的一阶直觉主义逻辑的计算解释，提出了一种新的可靠而完备的语义.此外，一个健全的和完整的语义相应的Alzoda-calculus的派生，太。这种语义学在某种程度上扩展了由Heyting范畴、拓扑理论解释和Kripke模型给出的更传统的意义。证明引入这种新颖语义的特征是它是“无点”的事实，即，没有一个宇宙的元素被用来解释逻辑术语。换句话说，术语并不表示某些集合的个体，而是表示将语句的解释保持在一起的“胶水”，类似于形式拓扑中发生的情况。由于所提出的语义学可以平凡地扩展到所有基于直觉主义系统的一阶逻辑理论（并且，稍微注意一下，也可以扩展到最小系统），所以语义学也涵盖了所有的谓词理论，即使这些理论的一些特殊方面应该被注意到。
2013-06-29 cs.LO math.LO
One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus
该研究针对简单类型λ演算的反合一问题，突破现有研究仅关注禁止泛化变量嵌套的幺正变体的局限，证明含嵌套泛化变量时该问题为零元，为泛化方法的扩展应用提供理论支撑。
2024-03-15 cs.LO
Strategies as Resource Terms, and their Categorical Semantics
本文用增广因果结构直接刻画正规资源项与 Hyland-Ong 博弈的对应，并构造归约不变的资源演算指称模型及资源范畴。
2025-10-15 cs.LO
Semantics of Higher-Order Quantum Computation via Geometry of Interaction
虽然目前对量子计算的大部分研究都采用了诸如量子电路之类的低级形式，但最近已经提出了几种针对结构化量子编程的高级语言/演算。目前的工作有助于这些语言的语义研究提供基于交互的语义的功能量子程序设计语言;后者是，很像塞林格和Valiron的，基于线性λ演算，并配备了功能，如！模态和递归。所提出的指称模型是第一个支持量子功能程序设计语言的全部功能，我们证明我们的语义充分。我们的模型的建设是由一系列现有的技术，从经典计算的语义，以及从过程理论。其中最值得注意的是Girard的相互作用几何（GoI），由Abramsky，Haghverdi和Scott明确阐述。这些技术的数学通用性-主要是由于它们的分类公式-被利用来帮助我们从经典到量子。
2016-05-17 cs.LO
Enriched Categories for Parameterized Circuit Semantics
本文用充实范畴和内部构造统一理解参数化量子电路语义，给出产生对称幺半范畴的充分条件，并展望扩展到经典电路与等价性检查。
2025-01-21 cs.LO quant-ph
