Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
本文将对偶演算推广为归纳型和余归纳型。本文首先介绍了一个非确定性的对偶演算的归纳和共归纳类型。它除了具有原对偶演算的对偶性外，还具有归纳型和余归纳型的对偶性，即归纳型和余归纳型的项和余项的对偶性及其归约规则的对偶性。它的强正规化也被证明，这是通过将其转化为一个二阶对偶演算。通过将二阶对偶演算转化为二阶对称λ演算，证明了二阶对偶演算的强正规化。本文接着介绍了归纳型和共归纳型对偶演算的按值调用系统和按名调用系统，并说明了按值调用和按名调用的对偶性、Church-Rosser性质和强规范性。通过将它们转化为具有归纳和共归纳类型的非确定性对偶演算，证明了它们的强规范化性。
2013-03-27 cs.LO cs.PL
Type-Theoretic Signatures for Algebraic Theories and Inductive Types
本文将特定类型理论作为代数理论和归纳类型的规范语言，利用依赖类型理论描述了有限商归纳-归纳理论、其无限推广及更高归纳-归纳理论三类代数理论的语法与语义。
2023-09-10 cs.LO
Extending the Calculus of Constructions with Tarski's fix-point theorem
我们建议使用塔斯基的最小不动点定理作为基础，定义递归函数的演算归纳建设。这拓宽了可以在基于类型理论的定理证明工具中建模的函数类到潜在的非终止函数。这只有在我们通过增加与经典逻辑相对应的公理来扩展逻辑框架时才有可能。我们声称，扩展的框架使得有可能终止和非终止计算的原因，我们表明，共同设施的演算的归纳建设，如程序提取可以扩展到也处理新的功能。
2006-10-11 cs.LO
LPC(ID): A Sequent Calculus Proof System for Propositional Logic Extended with Inductive Definitions
Carnegie Mellon University（卡内基梅隆大学）；Katholieke Universiteit Leuven（鲁汶大学）
逻辑FO（ID）使用来自逻辑编程领域的思想来扩展具有非单调归纳定义的一阶逻辑。这种逻辑形式上扩展了逻辑程序设计、溯因逻辑程序设计和数据逻辑，从而将对这些形式主义的看法形式化为（广义）归纳定义的逻辑。本文的目标是研究FO（ID）的命题片段PC（ID）的演绎推理方法。我们引入了一个正式的证明系统的基础上的演算（根森式演绎系统），这种逻辑。由于PC（ID）是经典命题逻辑和命题归纳定义的集成，我们的推理演算证明系统集成了命题演算和定义的推理规则。我们提出了这个证明系统的可靠性和完整性，相对于PC（ID）的一个略有限制的片段。我们还提供了PC（ID）的一些复杂性结果。通过对PC（ID）证明系统的开发，有助于加深对FO（ID）证明理论基础的理解，从而研究FO（ID）的有效证明系统。
2012-07-11 cs.AI cs.LO
Complete Bidirectional Typing for the Calculus of Inductive Constructions
本文提出了一个归纳结构演算（CIC）的双向类型系统。它引入了一种介于通常的推理和检查之间的新判断，称为约束推理，以处理类型中的计算。该系统的关键属性是其相对于通常的无向系统的完备性，这已经在Coq中作为MetaCoq项目的一部分正式证明。虽然它在一个现实的类型化算法的持续完整性证明中扮演着重要的角色，但双向性的兴趣更广泛，因为它在试图证明CIC或设计变体和扩展的属性时提供了见解和结构。特别是，我们提出了约束推理，通常的推理和检查判断之间的中间，处理类型中的计算的存在。
2021-04-19 cs.LO cs.PL
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
本文提出了一种基于逻辑演算的证明方法，结合归纳定义的谓词表示的有界树宽结构和理论推理，检验分离逻辑公式之间蕴涵的有效性。微积分是可靠的和完备的，在这个意义上，证明树是有效的当且仅当它允许一个（可能是无限的）证明树。我们表明，该过程在以下两种情况下终止：（i）当归纳规则，定义谓词发生在左手边的蕴涵终止，在这种情况下，证明树总是有限的。(ii)当理论是空的，在这种情况下，每个有效的证明树都允许一个有理证明树，其中在证明树中出现的成对不同序列的总数是关于r.t.的双指数。最后的结局。
2022-06-22 cs.LO
The algebraic $λ$-calculus is a conservative extension of the ordinary $λ$-calculus
该研究纠正了代数λ-演算对普通λ-演算保守性结论的过往错误证明，解释旧方法失效原因，提出新技术证明两普通λ-项在代数λ-演算中等价当且仅当β-相等。
2023-06-15 cs.LO
Confluence via strong normalisation in an algebraic λ-calculus with rewriting
线性-代数演算和代数演算是用任意线性组合项扩展的无类型代数代数演算。前者以重写系统的形式呈现线性代数的公理，而后者使用等式。当重写时，代数演算不是融合的，除非增加进一步的限制。我们提供了一个类型系统的线性代数演算强制执行强规范化，这给回汇合。类型系统允许在系统F中进行抽象解释。
2012-03-28 cs.LO
A Deductive Refinement Calculus for Differential-Algebraic Programs
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；Carnegie Mellon University（卡内基梅隆大学）
本文提出微分代数细化逻辑(dARL)，用于演绎验证微分代数程序的属性与关系。通过引入新型轨迹基于语义，实现复杂微分代数方程的逐步验证与简化，确保每一步的正确性。
2026-05-11 cs.LO
Semantics of a Typed Algebraic Lambda-Calculus
代数代数演算已经以各种方式进行了研究，但它们的语义大多未被触及。本文给出了一个具有向量空间结构的一般单型λ演算的语义分析。我们用两个已建立的向量代数演算来描述这种关系。然后我们研究了不动点组合子的加法所引起的问题以及如何修正方程理论来解决这些问题。我们勾勒出一个代数矢量PCF和它可能的指称解释。
2010-06-08 cs.LO
Clone Theory: Its Syntax and Semantics, Applications to Universal Algebra, Lambda Calculus and Algebraic Logic
本文的主要目的是提出一种统一的方法，将逻辑系统的语法转化为一定的初始代数结构，以便用代数的方法来研究它。为此目的人们可以选择的代数结构是一个范畴的一个完整子范畴上的各种克隆。证明了方程逻辑、λ演算和一阶逻辑的语法都可以表示为正整数集合上的克隆或克隆的右代数。语义，然后表示来自这些克隆左代数的结构。
2008-10-17 cs.LO
An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions
KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文为 FO(ID) 逻辑中的非单调归纳定义形式化了无限下降原理，通过扩展 LKID{\omega} 和 CLKID{\omega} 得到相继式演算 SCFO(ID)-inf 和 SCFO(ID)-cyc，并证明了可靠性、完备性、消割及与 SCFO(ID) 的关系。
2026-09-23 cs.LO math.LO
Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
我们研究了代数演算，微分代数演算的一个片段和线性代数代数演算，量子计算的候选代数代数演算之间的关系。这两个演算都是代数的：每一个都配备有加法和标量乘法结构，并且它们的项集合在线性组合下是封闭的。然而，这两种语言是使用不同的方法构建的：前者是按名称调用的语言，而后者是按值调用的语言;前者考虑代数等式，而后者通过重写规则来处理它们。在本文中，我们分析这些不同的方法是如何相互关联的。为此，我们提出了四个规范语言的基础上，每一个可能的选择：调用的名称与调用的值，代数等式与代数重写。我们表明，各种语言相互模拟。由于beta归约和代数重写之间的微妙相互作用，为了使语言保持一致，可能需要一些额外的假设，如融合或规范化。我们仔细设计了每个证明所需的属性，使它们足够通用，对满足相应属性的任何子语言都有效。
2014-12-09 cs.LO
A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
我们描述了一个类型系统的线性代数λ演算。类型系统解释了语言中模拟线性运算符和向量的部分，也就是说，它能够静态地描述程序归约所产生的项的线性组合。这就产生了一个原始的类型论，在这个理论中，类型可以像项一样叠加成线性组合。我们表明，所得到的类型的λ演算是强规范化和功能弱主题减少。
2012-07-31 cs.LO
Definitions by Rewriting in the Calculus of Constructions
本文的主要新颖之处是考虑扩展的演算的建设，谓词可以定义一个一般形式的重写规则。我们证明了强规范化的约简关系产生的beta规则和用户定义的规则下，一些一般的句法条件，包括合流。作为例子，我们表明，两个重要的系统满足这些条件：一个子系统的演算的归纳结构的基础上的证明助手Coq，和自然演绎模一个大类的方程理论。
2006-10-11 cs.LO
Sequent Calculus and Equational Programming
基于类型论的证明助手和程序设计语言通常有两种风格：一种是基于类型论的标准自然演绎表示，并涉及消除器，而另一种是提供等式风格的语法。我们在这里表明，方程的方法对应于使用一个集中的介绍类型论表示为微积分。一个类型化的函数语言，基于一个代数演算，我们涉及到的语法和内部语言的Agda。特别是，我们讨论了使用的模式和情况下分裂，以及规则实现归纳推理和相关产品和总和。
2015-07-29 cs.LO
Dedukti: a Logical Framework based on the $λ$$Π$-Calculus Modulo Theory
本文介绍逻辑框架Dedukti，它基于模理论的$\lambda$$\Pi$-演算，能表达多种逻辑理论并检查其他证明系统（如Zenon、HOL Light等）的大型证明库。
2023-11-13 cs.LO
Inductive-data-type Systems
在以前的工作（“抽象数据类型系统”，TCS 173（2），1997），最后两位作者提出了一个组合的语言（强规范化）代数重写系统和类型化的代数演算丰富的模式匹配定义遵循一定的格式，称为“一般模式”，它概括了通常的递归定义为自然数和类似的“基本归纳类型”。这种组合语言被证明是强烈的规范化。本文的目的是重新制定和扩展的一般模式，以使其易于扩展，以捕获更一般的类的归纳类型，称为“严格正”，并减轻强规范化证明的结果系统。这一结果提供了一个计算模型的组合的代数规约语言的基础上抽象数据类型和强类型的功能语言，严格积极的归纳类型。
2013-09-16 cs.LO
Initial Algebras of Domains via Quotient Inductive-Inductive Types
Radboud University（拉德堡德大学）；Technical University Eindhoven（埃因霍温理工大学）
本文通过商归纳-归纳类型构造域的初始代数，用于在域理论中建模代数效应。
2026-02-27 cs.LO
A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文提出实解析微分代数动态逻辑的证明演算，用于正确转换微分代数方程，实现微分代数方程到常微分方程的降阶，并确保与混合系统中的微分形式动态逻辑兼容。主要贡献是鬼切换，用于将多模系统分解为混合系统，正确混合复杂的微分代数动力学。
2025-05-25 cs.LO
Inductive Reasoning for Coinductive Types
本文提出 AlgCo 框架，利用代数完全偏序和稠密集合上的原始递归，实现对 conats、流等余归纳类型的归纳推理，并在 Coq 中验证了筛法、正则表达式库和概率采样语义。
2023-04-07 cs.LO
A Diagrammatic Calculus for Algebraic Effects
我们引入一个新的图形符号表示（代数）有效计算的结果。我们的表示法明确地将计算过程中产生的影响与可能返回的值分开，这样就简化了纯计算的定义和结果的扩展，使其成为有效的设置。此外，我们显示了一些代数和秩序理论的法律图，这种方式奠定了基础的代数效果的图解演算。我们给出了一个正式的基础，这样的演算的Lawvere理论和通用效果。
2020-01-07 cs.LO cs.PL
Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution
我们提出了一个完整的形式化的标准化定理的Martin-Löf的构造类型论的λ演算使用一阶语法与一种名称的自由和绑定变量和斯托顿的多重替代。我们的形式化是基于Ryo Kashima的证明，其中具有标准序列的beta-约简的概念被归纳关系捕获。证明只使用结构归纳法的语法和定义的关系，这是可能的，由于我们采用的特定公式的替代。整个开发过程使用Agda系统进行了机器检查。
2018-07-05 cs.LO
The Vectorial $λ$-Calculus
我们描述了线性代数$λ$演算的一个类型系统。类型系统解释了$λ$ -演算的扩展的线性代数方面：它能够静态地描述当减少程序时将获得的项的线性组合。这就产生了一个原始的类型论，在这个理论中，类型可以像项一样叠加成线性组合。我们证明了所得到的类型$λ$ -演算是强正规化的，并具有弱主题约简的特征。最后，我们将展示如何在这种类型的演算中自然地编码矩阵和向量。
2017-04-17 cs.LO
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
我们在这里研究了一个新版本的归纳构造演算（CIC），证明助手Coq是基于它的：一致归纳构造演算，它通过构建任意的一阶决策过程来真正扩展CIC：deduction仍然负责CIC内核，而计算则外包给专用的一阶决策程序，这些程序可以从货架上取下来，只要它们提供证明证书。整个系统的可靠性是证书检查器和内核可靠性的增量属性。一个详细的例子表明，由此产生的证明风格变得更接近工作数学家。
2008-04-23 cs.LO
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
Microsoft Research-INRIA Joint Centre（微软研究院-法国国家计算机科学与自动化研究所联合中心）
介绍了在交互式定理证明器Matita中实现的（共）归纳构造演算（CIC）的精化算法。精化算法负责为用户直接编写或使用策略、决策过程或通用自动化生成的术语、类型和证明术语赋予含义。这些术语是以“外部语法”编写的，这意味着用户友好，允许省略信息，无类型的绑定器和用户定义的子类型的某种自由使用。细化器修改这些项以获得ITP的内核所理解的内部语法中的相关良好类型的项。特别地，当所有绑定器都是无类型的时，它充当类型推断算法。所提出的算法是双向的：给定外部语法中的术语和该术语所期望的类型，它将尽可能多的类型信息传播到术语的叶子。相反，传统的单向算法以自下而上的方式进行，通过推断子项的类型并仅在最后将其与其上下文所期望的类型进行比较（统一）。我们提出了一些新的双向规则CIC是特别有效的。在双向性的好处中，我们有更好的错误消息报告和更好的依赖类型推断。此外，由于双向性，用于子类型化的强制系统更有效，并且类型推断生成更简单的统一问题，这些统一问题更可能由所实现的固有不完整的高阶统一算法来解决。最后，我们在外部语法中引入了占位符向量的概念，它可以同时省略任意数量的参数。占位符向量允许隐式参数的简单实现，并大大简化了原始和简单策略的实现。
2012-03-01 cs.AI cs.LO
The Rooster and the Syntactic Bracket
我们提出了一个扩展的纯型系统的代数表示的诱导和共诱导型家庭适当的指标。这种类型论支持通过显式类型构造以及非谓词排序从较小的排序到较大的排序的扩展。非谓词排序中的类型族是用括号操作构造的。从非谓词排序到类型的模式匹配的必要限制仅限于括号结构。这种类型论给出了一个替代介绍归纳结构的演算上的Coq证明助手是一个实现。
2014-06-13 cs.LO
On the relative power of algebraic approximations of graph isomorphism
我们比较了两种方法来近似图同构使用线性代数方法的能力：\emph{invertible map tests}（由Dawar和Holm介绍）和证明系统与代数规则，即\emph{polynomial calculus}，\emph{monomial calculus}和\emph{Nullstellensatz calculus}。在特征为零的域的情况下，这些变体本质上都等价于Weisfeiler-Leman算法。在积极的特点，我们表明，可逆映射方法可以模拟单项演算，并确定一个潜在的方式来扩展到单项演算。
2021-03-30 cs.LO math.CO
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
Inria（法国国家信息与自动化研究所）；Université Nantes（南特大学）；Ben-Gurion University of the Negev（内盖夫本-古里安大学）；Saarland University（萨尔大学）；MPI-SWS（马克斯·普朗克软件系统研究所）
本文在归纳构造演算中基于序列连续性发展了预言机可计算性与图灵可归约性的综合概念，并在 Coq 中完成机器检查，证明了图灵可归约性构成上半格、传递可判定性且强于真值表可归约性。
2023-07-28 cs.CL cs.LO math.LO
Completeness of algebraic CPS simulations
代数λ演算和线性代数λ演算是经典λ演算的两种线性组合推广。它们在不同的背景下独立出现：前者是微分λ演算的一个片段，后者是量子计算的候选λ演算。它们在应用程序参数和代数规则的处理上有所不同。这两种语言可以使用著名的按值调用和按名称调用CPS翻译的代数扩展来相互模拟。这些模拟是合理的，因为它们保留了减少。在本文中，我们证明了模拟实际上是完整的，加强了两种语言之间的联系。
2012-07-31 cs.LO quant-ph
Two linearities for quantum computing in the lambda calculus
我们提出了一种方法来统一量子代数演算中的两种非克隆方法：逻辑线性和代数线性。第一种方法是禁止重复变量，而第二种方法是将所有的非线性项都视为代数线性函数。我们通过定义一阶简单类型的量子扩展来说明这个想法，其中类型在叠加上是线性的，同时允许克隆基向量。此外，我们提供了一个解释的演算叠加类型被解释为向量空间和非叠加类型作为其基础。
2019-07-31 cs.LO
Canonicity results for mu-calculi: an algorithmic approach
研究了直觉μ-演算不等式的规范性。在存在不动点算子的情况下，规范性的概念并不完全简单。在规范扩展的代数设置中，我们研究了规范性的通常概念和我们称之为驯服规范性的概念。后一个概念以前已经被Bezhanishvili和Hodkinson研究了经典的μ演算。我们的方法是在萨尔奎斯特理论的精神。也就是说，我们确定语法定义类的不等式，即限制归纳和驯服归纳不等式，这是，分别是典型的或驯服典型的。我们的方法是使用一种算法，处理的目的是消除命题变元的不等式。我们介绍的算法是密切相关的算法ALBA和穆ALBA研究Conradie，Palmigiano等人。它是基于演算的重写规则，其可靠性取决于代数嵌入到他们的规范扩展和秩序理论的性质，后者。我们表明，该算法成功的每一个限制归纳不等式通过一个所谓的适当的运行，这是足以保证他们的正规性。同样，我们能够证明算法成功的每一个驯服的归纳不等式通过所谓的驯服运行。反过来，这保证了他们驯服的正规性。
2014-08-27 cs.LO math.LO
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
Type Theory with Single Substitutions
本文为类型理论定义了仅含单一替换和弱化的单一替换演算（SSC），证明了其语法与带族范畴（CwF）语法同构，为定义类型理论提供了极简替代方案。
2025-10-14 cs.LO
Expressing the cone radius in the relational calculus with real polynomial constraints
我们表明，有一个查询表示在一阶逻辑上的reals，返回，在任何给定的半代数集A，对于每一个点的半径A是圆锥形的。我们得到这一结果结合著名的结果从微积分和真正的代数几何，特别是萨尔德定理和汤姆的第一个合痕引理，最近的算法结果Rannou。
2001-06-21 cs.DB cs.LO
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
自从Val Tannen的先驱工作简单类型的类演算和一阶重写的组合（LICS'88），许多作者都通过将其扩展到更丰富的类型类演算和重写范式，最终在演算像代数结构的演算。这些工作提供了理论基础的类型理论的证明助手的功能和谓词定义的定向高阶方程。这种定义包含了基于归纳的定义，更容易编写，并提供了更多的自动化。另一方面，检查用户定义的重写规则是强规范化和融合的，并且在与beta约简结合时保持类型检查的可判定性，则更加困难。大多数终止标准依赖于期限结构。在以前的工作中，我们扩展到依赖类型和高阶重写，“大小类型”的概念由几位作者在ML类语言的简单框架中研究，并证明了它保持了强规范化。本文件的主要贡献是双重的。首先，证明了在带尺寸标注的代数构造演算中，只要尺寸标注所产生的约束集是可满足的，并且允许最一般的解，则类型推断和类型检验问题是可判定的.其次，我们证明了一个大小代数足够丰富的捕获通常的归纳为基础的定义和更多的后来的属性。
2006-09-11 cs.LO cs.PL
Type Theory based on Dependent Inductive and Coinductive Types
我们开发了一个依赖的类型论，纯粹基于归纳和共归纳类型，以及相应的递归和共递归原则。这就产生了一个只有少量规则集的类型论，同时仍然具有相当的表达能力。例如，所有众所周知的基本类型和类型的形式，需要使用这个类型论作为一个逻辑是可定义的：命题连接词，如虚假，合取，析取，和功能空间，依赖功能空间，存在量化，平等，自然数，向量等。众所周知的类型的归约关系由此产生。为了进一步支持这个新的类型论的引入，我们还证明了它的项演算的基本性质。最重要的是，我们证明了主题减少和强规范化的减少关系，这使得计算意义的条款。所提出的类型论是基于第一作者以前研究过的分类逻辑的思想，它将Hagino的分类数据类型扩展到依赖类型化的设置。通过将类型论建立在范畴论的概念上，我们保持了归纳类型和上归纳类型之间的对偶性，并且它允许我们将函数空间描述为上归纳类型。
2016-05-07 cs.LO
Typed lambda-terms in categorical attributed graph transformation
本文讨论了基于属性图重写的模型转换。我们的贡献调查一个单一的推出方法应用重写规则。图的属性的计算是通过使用归纳类型的类型化演算来实现的。在本文中，我们提出了解决方案，以应付单推出建设的图形结构和计算功能。由于该重写系统使用归纳类型，属性计算的表达性得到了促进，并且比基于Sigma代数的重写系统更有效。本文描述了一些例子，显示我们的计算方法的兴趣。
2011-06-30 cs.LO
A concrete model for a typed linear algebraic lambda calculus
本文为带测量的类型化线性代数 lambda 演算 Lambda-S 构造了基于集合与复向量空间范畴伴随关系的具体模型，用隐藏的遗忘函子解释叠加类型 S。
2023-10-11 cs.LO math.LO
Limitations of Algebraic Approaches to Graph Isomorphism Testing
我们研究了基于代数推理技术的图同构算法，如格罗布纳基计算。这些算法的思想是将两个图编码成一个方程组，当且仅当图是同构的时，方程组是可满足的，然后使用例如格罗布纳基算法来（尝试）确定系统的可满足性。在某些情况下，这可以在多项式时间内完成，特别是，如果方程在代数证明系统（如Nullstellenetron或多项式演算）中允许有界度反驳。我们证明了线性下界的多项式演算度在所有领域的特征不同于2，也线性下界的程度Positivstellenbrand演算导子。我们比较这种方法最近研究的线性和半定规划方法同构测试，这是已知的组合Weisfeiler-Lehman算法。我们确切地证明了Weisfeiler-Lehman算法在代数证明系统方面的能力，该代数证明系统位于k度Nullstellenetrance和k度多项式演算之间。
2015-02-20 cs.CC cs.LO
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
这项工作利用会话类型的逻辑基础，以确定什么样的类型纪律的π演算可以准确地捕获，并被捕获，π演算的行为。利用证明理论的内容的可靠性和完整性的微积分和自然演绎呈现的线性逻辑，我们开发了第一个相互逆和完全抽象的进程作为函数和函数作为进程编码之间的多态会话π演算和系统F的线性制定。然后，我们能够从会话演算的理论推导出会话演算的结果：（1）我们通过系统F中的代数表示获得归纳和共归纳会话类型的特征;（2）我们将结果扩展到值和进程传递，需要强规范化。
2018-01-25 cs.LO cs.PL
Lineal: A linear-algebraic Lambda-calculus
我们提供了向量空间和双线性函数的概念的计算定义。我们使用这个结果来介绍一个最小的语言相结合的高阶计算和线性代数。这种语言扩展了λ演算，使之有可能进行α t + β u项的任意线性组合。我们描述了如何“执行”这个语言的一些重写规则，并证明他们通过两个基本要求，语言是一个语言的线性运算符，它是高阶。我们提到的角度，这项工作在量子计算领域，其电路，我们可以很容易地编码在微积分。最后，我们证明了整个演算的汇合。
2017-03-21 cs.LO cs.PL quant-ph
From Semantics to Types: the Case of the Imperative lambda-Calculus
我们提出了一个交叉型系统的一个强制性的基于状态单子和代数运算的演算读取和写入存储。该系统是通过求解一个合适的域方程的欧米茄代数格的范畴;该解决方案包括一个过滤器模型推广了著名的建设普通的λ演算。然后，类型系统从过滤器模型本身的术语解释中获得。这样得到的类型系统满足“类型语义”属性，并且通过构造它是可靠的和完备的。
2021-12-28 cs.LO cs.PL
Inductive types in homotopy type theory
同伦类型论（英语：Homotopy type theory）是马丁-勒夫的构造性类型论在抽象同伦理论中的一种解释。有结果之间的联系建设性数学和代数拓扑，提供拓扑语义内涵系统的类型理论，以及计算方法，代数拓扑通过类型理论为基础的证明助手，如Coq。目前的工作调查归纳类型在这种情况下。修改规则的归纳类型，包括类型的良基树，或W型，提出了，并确定了基本的同伦语义，这样的类型。所有结果的证明都已由Coq证明助理正式验证，并且用于此验证的证明脚本构成了本研究的重要组成部分。
2012-05-02 cs.LO math.CT math.LO
A System F accounting for scalars
代数演算和线性代数演算扩展了代数演算，使其可以进行任意的线性组合。在本文中，我们提供了一个细粒度的，系统F型系统的线性代数演算。我们表明，这个“标量”型系统享有的主题还原属性和强规范化属性，我们的主要技术成果。后者产生了一个显着的简化的线性代数微积分本身，通过消除需要的一些限制，在其减少规则。但是，这个标量类型系统更重要的原始特性是，它跟踪每个术语中存在的“类型的数量”。作为一个使用的例子，我们证明了它可以保证一个项的范式是重心的，即它的标量和为1。
2012-02-28 cs.LO cs.PL quant-ph
Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants
DeepThought Solutions（深思科技）；Department of Computer Science University of Florida（佛罗里达大学计算机科学系）
本文提出通过代数不变量实现LLMs的结构归纳-演绎-演绎推理框架，通过五种代数不变量确保推理链中结论的可靠性，防止逻辑不一致的累积。
2026-04-17 cs.AI cs.LG cs.LO
Uniform Proofs of Normalisation and Approximation for Intersection Types
我们提出了交叉型系统的风格的微积分，修改的系统，瓦伦蒂尼介绍了证明规范化属性，而不使用reductionmethod。我们的系统比Valentini的系统更自然，相当于通常的自然演绎风格的系统。我们证明的特征定理的强和弱规范化，通过建议的系统，而且，通过直接的归纳论点的近似定理。这提供了一个统一的方式证明的规范化和近似定理通过类型系统在微积分风格。
2015-03-17 cs.LO cs.PL
Algebraic models of simple type theories: a polynomial approach
我们开发简单的类型论的代数模型，奠定了一个框架，扩展通用代数，将代数排序和变量绑定。简单类型论的例子包括单位类型和简单类型的$λ$ -演算、计算$λ$ -演算和谓词逻辑。简单类型论是在预层范畴中给出的模型，其结构由对应于自然演绎规则的多项式内函子的代数指定。我们构建的初始模型抽象地描述了简单类型论的语法。考虑到替换结构，我们进一步提供了结构化carbohydrate多范畴的声音和完整的语义。这一发展概括了Lambek的对应关系之间的简单类型$λ$演算和笛卡尔闭范畴，任意简单的类型论。
2020-06-30 cs.LO math.CT
A standardisation proof for algebraic pattern calculi
这项工作提供了一些见解和结果的标准化呼叫的名称模式演算。更确切地说，我们定义了一个基于构造器的数据项和模式的模式演算的标准约简。这个概念是基于减少步骤，需要匹配一个参数相对于一个给定的模式。本文利用Takahashi和Crary发展起来的方法证明了标准化定理。证明是基于这样一个事实，即任何发展可以指定为一系列的头部步骤，其次是内部减少，即减少，其中没有头部步骤参与。
2011-02-18 cs.LO cs.PL
Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus
本文从范畴和代数的角度研究了类型化λ演算的赋值正规化问题。本文的第一部分通过Kripke逻辑关系分析了Jung和Tiuryn的lambda可定义性结果，并展示了它如何适用于统一可定义性和规范化，产生一个扩展的规范化结果。在第二部分的文件的分析进一步细化考虑内涵Kripke关系（在阿丁胶合的形式），并显示提供一个功能的规范化条款，铸造规范化的范畴胶合的背景下进行评估。技术发展包括类型化λ演算的语法和语义的代数处理，其允许在简单类型化元理论内给出规范化函数的定义。合成依赖类型的函数式程序设计语言中的求值规范化程序。
2022-08-18 cs.LO math.CT
Fuzzy Algebraic Theories
在这项工作中，我们提出了一个正式的系统模糊代数推理。我们定义的模糊演算是基于两种命题，捕捉平等和存在的条款作为模糊集的成员。我们提供了一个健全的语义，这种演算，并表明，有一个概念，在这个系统中的任何理论的自由模型，使我们（有一些限制）恢复模型作为一些单子的Eilenberg-Moore代数。我们还将证明一个完备性结果：一个公式是从一个给定的理论推导出来的，当且仅当它被该理论的所有模型所满足。最后，利用Milius和Urbat的结果，我们给出了代数的子范畴的类HSP特征，这些子范畴是特定种类的理论的模型范畴。
2021-10-21 cs.LO math.CT math.LO
Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi
University of Oxford（牛津大学）
本文提出图示代数几何（GAG），扩展了图示线性代数程序，证明其在代数结构的（co）span语义下是通用且完整的，展示了GAG在多项式约束网络中的重写系统应用及对量子计算中qudit ZH算子的扩展。
2026-05-13 cs.LO math.CT quant-ph
