Building Decision Procedures in the Calculus of Inductive Constructions
人们普遍认为，未来的证明助手的成功将依赖于他们在演绎中结合计算的能力，以便在用从P获得的等价命题P'的证明替换命题P的证明时模仿数学家，这可能是由于复杂的计算。在本文中，我们研究了一个新的版本的演算的归纳结构，其中包括任意的决策过程，通过转换规则的演算演绎。在归纳构造演算的背景下，问题的新颖性在于，计算机制随着证明检查而变化：目标与当前上下文中可用的用户假设集一起发送到决策过程。我们的主要结果表明，这种扩展的演算的建设不妥协的主要性质：汇合，主题减少，强规范化和一致性都被保留。
2007-07-09 cs.LO
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
本文将对偶演算推广为归纳型和余归纳型。本文首先介绍了一个非确定性的对偶演算的归纳和共归纳类型。它除了具有原对偶演算的对偶性外，还具有归纳型和余归纳型的对偶性，即归纳型和余归纳型的项和余项的对偶性及其归约规则的对偶性。它的强正规化也被证明，这是通过将其转化为一个二阶对偶演算。通过将二阶对偶演算转化为二阶对称λ演算，证明了二阶对偶演算的强正规化。本文接着介绍了归纳型和共归纳型对偶演算的按值调用系统和按名调用系统，并说明了按值调用和按名调用的对偶性、Church-Rosser性质和强规范性。通过将它们转化为具有归纳和共归纳类型的非确定性对偶演算，证明了它们的强规范化性。
2013-03-27 cs.LO cs.PL
The Calculus of Algebraic Constructions
本文讨论了代数构造演算（CAC）的基础，CAC是构造演算的归纳数据类型的扩展。CAC通过模式匹配提供函数的定义来概括配备高阶原始递归的归纳类型，该模式匹配捕获满足严格正性条件的任意非依赖和非多态归纳类型的递归定义。CAC还通过提供依赖类型和高阶重写规则来概括抽象数据类型的一阶框架。
2008-05-27 cs.LO
Complete Bidirectional Typing for the Calculus of Inductive Constructions
本文提出了一个归纳结构演算（CIC）的双向类型系统。它引入了一种介于通常的推理和检查之间的新判断，称为约束推理，以处理类型中的计算。该系统的关键属性是其相对于通常的无向系统的完备性，这已经在Coq中作为MetaCoq项目的一部分正式证明。虽然它在一个现实的类型化算法的持续完整性证明中扮演着重要的角色，但双向性的兴趣更广泛，因为它在试图证明CIC或设计变体和扩展的属性时提供了见解和结构。特别是，我们提出了约束推理，通常的推理和检查判断之间的中间，处理类型中的计算的存在。
2021-04-19 cs.LO cs.PL
Extending the Calculus of Constructions with Tarski's fix-point theorem
我们建议使用塔斯基的最小不动点定理作为基础，定义递归函数的演算归纳建设。这拓宽了可以在基于类型理论的定理证明工具中建模的函数类到潜在的非终止函数。这只有在我们通过增加与经典逻辑相对应的公理来扩展逻辑框架时才有可能。我们声称，扩展的框架使得有可能终止和非终止计算的原因，我们表明，共同设施的演算的归纳建设，如程序提取可以扩展到也处理新的功能。
2006-10-11 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
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
本文提出了一种基于逻辑演算的证明方法，结合归纳定义的谓词表示的有界树宽结构和理论推理，检验分离逻辑公式之间蕴涵的有效性。微积分是可靠的和完备的，在这个意义上，证明树是有效的当且仅当它允许一个（可能是无限的）证明树。我们表明，该过程在以下两种情况下终止：（i）当归纳规则，定义谓词发生在左手边的蕴涵终止，在这种情况下，证明树总是有限的。(ii)当理论是空的，在这种情况下，每个有效的证明树都允许一个有理证明树，其中在证明树中出现的成对不同序列的总数是关于r.t.的双指数。最后的结局。
2022-06-22 cs.LO
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
Canonicity results for mu-calculi: an algorithmic approach
研究了直觉μ-演算不等式的规范性。在存在不动点算子的情况下，规范性的概念并不完全简单。在规范扩展的代数设置中，我们研究了规范性的通常概念和我们称之为驯服规范性的概念。后一个概念以前已经被Bezhanishvili和Hodkinson研究了经典的μ演算。我们的方法是在萨尔奎斯特理论的精神。也就是说，我们确定语法定义类的不等式，即限制归纳和驯服归纳不等式，这是，分别是典型的或驯服典型的。我们的方法是使用一种算法，处理的目的是消除命题变元的不等式。我们介绍的算法是密切相关的算法ALBA和穆ALBA研究Conradie，Palmigiano等人。它是基于演算的重写规则，其可靠性取决于代数嵌入到他们的规范扩展和秩序理论的性质，后者。我们表明，该算法成功的每一个限制归纳不等式通过一个所谓的适当的运行，这是足以保证他们的正规性。同样，我们能够证明算法成功的每一个驯服的归纳不等式通过所谓的驯服运行。反过来，这保证了他们驯服的正规性。
2014-08-27 cs.LO math.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
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
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
The Rooster and the Syntactic Bracket
我们提出了一个扩展的纯型系统的代数表示的诱导和共诱导型家庭适当的指标。这种类型论支持通过显式类型构造以及非谓词排序从较小的排序到较大的排序的扩展。非谓词排序中的类型族是用括号操作构造的。从非谓词排序到类型的模式匹配的必要限制仅限于括号结构。这种类型论给出了一个替代介绍归纳结构的演算上的Coq证明助手是一个实现。
2014-06-13 cs.LO
Algorithmic correspondence and analytic rules
本文引入算法MASSA，可从经典模态公式生成G3K的分析几何规则与无切割推导，证明其对分析归纳公式的终止性及对应性，还拓展至归纳公式与带量词模态逻辑。
2025-04-15 cs.LO math.LO
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
这项工作利用会话类型的逻辑基础，以确定什么样的类型纪律的π演算可以准确地捕获，并被捕获，π演算的行为。利用证明理论的内容的可靠性和完整性的微积分和自然演绎呈现的线性逻辑，我们开发了第一个相互逆和完全抽象的进程作为函数和函数作为进程编码之间的多态会话π演算和系统F的线性制定。然后，我们能够从会话演算的理论推导出会话演算的结果：（1）我们通过系统F中的代数表示获得归纳和共归纳会话类型的特征;（2）我们将结果扩展到值和进程传递，需要强规范化。
2018-01-25 cs.LO cs.PL
Type Theory with Single Substitutions
Eötvös Loránd University (ELTE)（罗兰大学）
本文为类型理论定义了仅含单一替换和弱化的单一替换演算（SSC），证明了其语法与带族范畴（CwF）语法同构，为定义类型理论提供了极简替代方案。
2025-10-14 cs.LO
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
Uniform Proofs of Normalisation and Approximation for Intersection Types
我们提出了交叉型系统的风格的微积分，修改的系统，瓦伦蒂尼介绍了证明规范化属性，而不使用reductionmethod。我们的系统比Valentini的系统更自然，相当于通常的自然演绎风格的系统。我们证明的特征定理的强和弱规范化，通过建议的系统，而且，通过直接的归纳论点的近似定理。这提供了一个统一的方式证明的规范化和近似定理通过类型系统在微积分风格。
2015-03-17 cs.LO cs.PL
Inductive Learning of Robot Task Knowledge from Raw Data and Online Expert Feedback
University of Verona（维罗纳大学）
针对复杂场景机器人任务先验知识缺失问题，提出从少量异构执行数据中归纳学习任务规范的离线算法，结合在线专家反馈增量优化知识，在外科机器人基准上验证了高效性与可扩展性潜力。
2025-01-13 cs.AI cs.LO cs.RO
Towards the average-case analysis of substitution resolution in $λ$-calculus
替换解析支持$β$ -归约的计算特性，通过避免捕获的绑定变量项交换来补充其执行。唉，替换的元级定义，掩盖了一个非平凡的计算，把$β$ -归约变成了一个原子重写规则，尽管它的操作复杂度不同。在本文中，我们提出了一个有点间接的平均情况下分析的替代决议在经典的$λ$演算，在$λ\upsilon$，一个扩展的$λ$演算内化的显式替代的$\upsilon$演算的替代定量分析的基础上。在这个框架内，我们表明，对于任何固定的$n \geq 0$，一个均匀随机的概率，条件的大小，$λ\upsilon$ -长期$\upsilon$ -规范化在$n$正常顺序（即最左最外）减少步骤往往是一个可计算的限制，长期大小趋于无穷大。为此，我们建立了一个有效的层次结构$\left(\mathscr{G}_n\right)_n$的定期树文法分区$\upsilon$ -规范化条款到类的条款规范化在$n$正常顺序重写步骤。在我们的建设的主要技术成分是一个归纳的方法来建设$\mathscr{G}_{n+1}$出$\mathscr{G}_n$的基础上，反过来，有限的交集分区的算法建设，罗宾逊的统一算法的启发。最后，我们简要地讨论了我们的方法的应用程序，其他长期重写系统，集中在两个密切相关的形式主义，即完整的$λ\upsilon$演算和组合逻辑。
2018-12-11 cs.LO math.CO
Parametricity in an Impredicative Sort
现在，对于一大类类型系统来说，Escherichold的抽象定理是一个很好的结果。本文给出了关系参量化的定义，并证明了Coq的基本形式语言归纳构造演算（CIC）中的抽象定理，其中参量化关系的余域是命题的非谓词类。为了继续下去，我们需要通过拆分排序层次结构来细化这个演算，以便将信息性术语与非信息性术语分开。这种细化非常接近CIC，但具有键入判断可以区分信息项的属性。在许多应用中，CIC内部的参数性的自然编码既有理论目的（证明命题相对于逻辑系统的独立性），也有实践目的（证明有限代数结构的性质）。最后，我们讨论了如何在我们的演算之上简单地构建一个新的自反Coq策略，该策略通过参数化来构造证明项。
2012-09-27 cs.LO
Efficient lambda encodings for Mendler-style coinductive types in Cedille
在依赖lambda消除演算（CDLE）中，可以通过lambda编码来定义归纳数据集，该编码具有常数时间析构函数和值过程归纳方案。本文首先讨论了对偶共归纳类型的缺失导子。我们的推导利用CDLE内的新方法，因为在适应以前已知的方法推导归纳类型似乎有根本的困难。我们提出的实现共归纳类型的lambda编码具有常数时间构造函数和一个值过程共递归方案。还支持共归纳类型族，支持许多标准共归纳属性的证明，例如流互模拟。所有工作都由Cedille工具（CDLE的一个实现）进行机械验证。
2020-05-01 cs.LO cs.PL
Touring the MetaCoq Project (Invited Paper)
证明助手在研究和工业中得到越来越广泛的使用，以提供关于理论、设计、系统和实现的经认证的和可独立检查的保证。然而，证明助手实现本身很少被验证，尽管它们在任何此类认证工作中占据了受信任代码库的主要份额。在这一领域，基于高阶逻辑的证明助手享有更强的保证，因为自认证实现已经有几年了。这种差异的一个原因是依赖类型论的内在复杂性，以及它们与归纳类型、论域多态性和复杂排序系统的扩展，以及理论与高效程序设计语言的实际实现之间的差距。MetaCoq是一个合作项目，旨在解决这些困难，为Coq证明助手底层的完整演算提供第一个经过完全认证的类型检查器的真实实现。为了实现这一点，我们改进了有时模糊的，如果不是不正确的，系统的规范和实现。我们展示了这个社区的理论工具，如双向类型检查，Tait-Martin-Löf/Takahashi的汇合证明技术和monadic和依赖类型编程，可以帮助构建以下工件：Coq的语法和类型论的规范，（Co）-归纳构造的多态累积演算（PCUIC）;用于操纵原始语法和与Coq系统交互的monad;对PCUIC的元理论的验证，其主要结果是归约、类型保持和类型原则的融合，PCUIC的一个真实、正确和完整的类型检查器，从PCUIC到无类型的类型演算的一个可靠的类型和证明擦除过程，即，辅酶Q提取机理的核心。
2021-07-16 cs.LO cs.PL
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille
Cedille是一个相对较新的工具，基于Curry风格的纯类型论，没有原始的数据类型系统。使用新技术的基础上依赖的交叉类型，归纳数据集及其归纳原则。这种方法的一个好处是它允许探索新的或高级形式的归纳数据类型。本文报告的工作进展中的一个这样的形式，即高阶抽象语法（HOAS）。我们在纯类型论的背景下考虑HOAS的性质，与传统的λ演算的环境模型的概念进行比较。我们看到了一种替代方案，基于我们所称的Kripke函数空间，我们可以在Cedille中推导出弱初始代数。使用编码给出了几个例子。
2019-10-24 cs.LO cs.PL
Finitary Simulation of Infinitary $β$-Reduction via Taylor Expansion, and Applications
本文将 Taylor 展开扩展至无穷 $λ$-演算 $Λ_{\infty}^{001}$，证明其可模拟无穷 $β$ 归约，并利用广义交换定理为该演算的规范化和合流性质提供了简单证明。
2023-12-19 cs.LO math.LO
ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
School of Information Science, Beijing Language and Culture University（北京语言文化大学信息科学学院）
提出ZX-演算，通过迹索引类型、预层非单调语义和构造性AGM信念修正，保守扩展Martin-Löf依赖类型论，并给出Coq机械化证明。
2026-06-02 cs.CL cs.LO
From signatures to monads in UniMath
术语UniMath既指数学的正式系统，也指在该系统中正式化的计算机检查的数学库。UniMath系统是一个依赖于核心的类型论，由univalence公理扩充。该系统保持尽可能小，以便于验证它-特别是，一般的感应类型不是系统的一部分。在这项工作中，我们通过从其他类型构造器中构造一些数据集及其相关的归纳原则来部分弥补归纳类型的不足。这涉及到一个范畴理论的结果的形式化的初始代数的建设，以及一种机制，方便地使用所获得的datastries。我们还将这种构造与先前的变量绑定语言的替换形式化相联系。总之，我们构建了一个框架，使我们能够简洁地指定，通过一个简单的概念绑定签名，变量绑定的语言。从这样一个规范，我们获得的数据类型的术语的语言，配备了一个认证的一元替换操作和一个合适的递归计划。使用这个，我们形式化无类型的λ演算和Martin-Löf类型论的原始语法。
2016-12-02 cs.LO cs.PL
A Logic for Reasoning About LF Specifications
我们提出了一个逻辑名为L_{LF}，其目的是正式的依赖类型的λ演算LF中开发的规范的属性。逻辑由构成规范的LF签名参数化。原子公式对应于相对于此签名的类型化派生。该逻辑包括命题连接词和量词的集合。量化范围在表示LF项和LF上下文的表达式上。第一种类型的量词由简单类型限定，这些类型描述与它们绑定的变量相关联的函数结构;更深层次的依赖相关属性由公式的主体表示。上下文级别的量词由上下文模式限定，上下文模式标识可以从中构造实际上下文的声明模式。无变量原子公式的语义通过它们编码的判断在LF中的可导性来表达。命题常量和连接词以通常的方式理解，量词的意义通过遵循类型限定的表达式替换来阐明。该逻辑由证明系统补充，该证明系统使得推理相对于所描述的语义是合理的。证明系统的主要新颖之处是提供了LF判断的案例分析式推理，支持LF推导高度的归纳推理和LF元定理的编码。该逻辑的动机是简单类型的λ演算中的类型分配的范例和证明系统说明通过形式化的类型唯一性证明这种演算。
2022-04-09 cs.LO cs.PL
Type-Based Termination for Futures
本文将顺序语言中的大小类型终止性检查方法适配到并发场景，通过扩展半公理化相继式演算提出大小类型细化方案，借助无限宽有限深的类型推导树和新颖逻辑关系论证，实现基于futures的函数式并发程序的终止性验证。
2024-04-15 cs.LO cs.PL
