Generating induction principles and subterm relations for inductive types using MetaCoq
我们在MetaCoq中实现了三个关于归纳类型的Coq插件。第一个插件是一个简单的语法转换，通过抽象构造函数类型中的具体索引来生成归纳类型的替代构造函数。第二个插件在MetaCoq中重新实现Coq的$\texttt{Scheme Induction}$命令，并将其扩展到嵌套归纳类型，例如在其定义中使用$\texttt{list}$的玫瑰树等类型，类似于Tassi的Elpi插件。第三个插件实现MetaCoq中Equations包提供的$\texttt{Derive Subterm}$命令。
2020-06-25 cs.LO
Signatures and Induction Principles for Higher Inductive-Inductive Types
本文提出一种基于签名理论的高阶归纳-归纳类型（HIITs）通用定义，支持多排序和等式构造子，并通过语法翻译计算归纳与递归原理，已在Agda中形式化并提供Haskell实现。
2020-02-12 cs.LO
Countability of Inductive Types Formalized in the Object-Logic Level
有限长的整数列表的集合和整数标号的二叉树的集合都是可数无限的。许多归纳定义的类型也有可数的元素。本文给出了Coq语言中一阶归纳定义的形式化语法，并证明了它们在一定条件下是可数的。我们没有用Meta语言编写证明生成器，而是在Coq对象逻辑中开发了一个无公理证明。换句话说，我们的证明是一个依赖类型的Coq函数，从归纳定义的语法到类型的可数性。在此基础上，我们提出了一种Coq策略来自动证明具体归纳类型的可数性。我们还为可数性和归纳定义的语法开发了Coq库，这些库本身就有价值。
2021-07-16 cs.LO
Constructing Infinitary Quotient-Inductive Types
本文介绍了一个表达类的服从-归纳类型，称为QW-类型。我们表明，在依赖的类型论与唯一性的身份证明，即使是无限的情况下，量子阱类型可以编码使用的组合，涉及严格的正发生的霍夫曼式商类型，和阿贝尔的大小类型的归纳-归纳定义。后者，这提供了一个方便的建设性的抽象什么经典将完成超限序数，被用来证明终止的递归定义的消除和计算性质，我们的编码的量子阱类型。使用Agda定理证明器对开发进行了形式化。
2020-02-19 cs.LO
The Size-Change Principle for Mixed Inductive and Coinductive types
本文针对嵌套归纳与余归纳类型，改进大小变化原理以检查递归定义的完全性，确保其相对于相应类型的正确性。
2025-09-02 cs.LO
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
Capretta的延迟单子可以用来模拟部分计算，但它有一个“错误”的概念，即内置的相等性，强双相似性。另一种方法是用“右”相等的概念，弱双相似性来商延迟单子。然而，查普曼等人最近的工作表明，如果不假设可数选择公理（的实例），就不可能在类型论的常见形式中定义一个单子结构。利用同伦类型论的一个思想--一种更高级的归纳-归纳类型--我们在不依赖可数选择的情况下构造了一个幺半群。我们证明了，在可数选择的存在下，我们的单变量等价于延迟单变量的弱双相似性。此外，我们概述了几个应用程序。
2017-06-27 cs.LO
Large and Infinitary Quotient Inductive-Inductive Types
Quotient inductive-inductive types（QIIT）是一种广义归纳类型，它允许在先前声明的排序上索引排序，并允许使用相等构造函数。QIIT对于类型论的代数描述和实数、序数和超实数的构造性定义特别有用。我们开发了新的元理论，大QIIT，大消除，递归方程和无穷构造。在以前的工作中，我们描述QIIT使用类型论，其中每个上下文代表一个QIIT签名。然而，在我们的例子中，签名理论也可以描述它自己的签名，模宇宙大小。我们引导的模型理论的签名使用自我描述和教会编码的签名的概念，而不使用复杂的原始语法或假设现有的内部QIIT的签名。我们给语义所描述的QIIT建模每个签名作为一个完全的CwF（类与家庭）的代数。与有限QIIT的情况相比，我们还需要在语义上证明代数同构下的不变性。我们通过将签名类型建模为isofibrations来做到这一点。最后，我们通过一个长期的模型建设表明，每一个QIIT是从签名理论的语法构造。
2020-06-23 cs.LO
Initial Algebras of Domains via Quotient Inductive-Inductive Types
Radboud University（拉德堡德大学）；Technical University Eindhoven（埃因霍温理工大学）
本文通过商归纳-归纳类型构造域的初始代数，用于在域理论中建模代数效应。
2026-02-27 cs.LO
Inductive types in the Calculus of Algebraic Constructions
在以前的工作中，我们证明了归纳构造演算（CIC）的一个重要部分，Coq证明助手的基础，可以被看作是代数构造演算（CAC），一个扩展的构造演算的功能和谓词定义的高阶重写规则。在本文中，我们证明了几乎所有的CIC可以被看作是一个CAC，它可以进一步扩展与非严格的积极类型和归纳递归类型与非自由构造函数和模式匹配定义的符号。
2006-10-12 cs.LO
Inductive types in the Calculus of Algebraic Constructions
在以前的工作中，我们证明了几乎所有的归纳构造演算（CIC），这是证明助手Coq的基础上，可以被看作是一个代数构造演算（CAC），一个扩展的构造演算的功能和谓词定义的高阶重写规则。在本文中，我们不仅证明了CIC作为一个整体可以被看作是一个CAC，但它也可以扩展与非自由的构造器，模式匹配上定义的符号，非严格正类型和归纳递归类型。
2006-10-11 cs.LO
Constructing (Co)inductive Types via Large Sizes
Leiden University（莱顿大学）；University of Amsterdam（阿姆斯特丹大学）
本文提出通过引入大尺寸类型和参数量化符来构造（co）归纳类型，解决了传统方法在一致性和模块性上的限制，并通过不可预测的现实模型证明了理论的一致性。
2026-04-30 cs.LO
A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories
在本文中，我们提出了一个形式化的Kozen的命题模态$μ$ -演算，在演算的归纳结构。我们解决了几个有问题的问题，如使用高阶抽象语法在归纳集合中存在的递归构造器，编码的模态（“证明”）规则和上下文敏感的语法。该编码可用于\Coq系统中，为$μ$ -演算中的无错证明的交互式开发提供了一个实验性的计算机辅助证明环境。我们采用的技术可以很容易地移植到其他语言和证明系统具有类似的问题。
1998-09-29 cs.LO
Positive Inductive-Recursive Definitions
提出了一种新的数据类型理论，它允许将类型定义为某些函子Fam（C）-> Fam（C）的初始代数.这个理论，我们称之为积极的归纳递归定义，是一个概括的Dybjer和Setzer的理论归纳递归定义内的C必须是离散的-我们的工作因此可以被视为解除这一限制。这是一个实质性的努力，因为我们不仅需要为这样的数据类型引入一种类型的代码（如Dybjer和Setzer的工作），而且还需要在这样的代码之间引入一种类型的态射（这在Dybjer和Setzer的开发中是不需要的）。我们展示了这些代码如何被解释为Fam（C）上的函子，以及这些代码的态射如何被解释为这些函子之间的自然变换。然后，我们给出了一个应用程序的积极的归纳递归定义的理论嵌套数据类型，我们给出了具体的例子，递归函数定义在宇宙中使用其消除原则。最后，我们证明存在的积极的归纳递归定义适应Dybjer和Setzer的集理论模型，我们的设置。
2015-03-26 cs.LO
Semantics for first-order affine inductive data types via slice categories
仿射类型系统是子结构类型系统，其中信息的复制受到限制，但在所有类型中允许丢弃信息。这种类型系统非常适合描述量子程序设计语言，因为量子信息的复制违反了量子力学定律。本文考虑了一个具有归纳数据类型的一阶仿射类型系统，并给出了它的一个新的范畴语义.这种解释最具挑战性的方面来自于为我们的数据类型构造适当的丢弃映射的需求，这些数据类型可能是由相互/嵌套递归定义的.我们展示了如何实现这一点，为所有类型的一阶线性类型系统的原子类型是可扩展的模型，然后提出了一个额外的仿射解释的类型内的切片类别的模型与张量单位。我们提出了一些具体的分类模型的语言，从经典的量子。最后，我们讨论了潜在的方法的二元化和扩展我们的方法，并使用它们来解释coalgebraic和懒惰的数据类型。
2020-01-19 cs.LO
Type Theory based on Dependent Inductive and Coinductive Types
我们开发了一个依赖的类型论，纯粹基于归纳和共归纳类型，以及相应的递归和共递归原则。这就产生了一个只有少量规则集的类型论，同时仍然具有相当的表达能力。例如，所有众所周知的基本类型和类型的形式，需要使用这个类型论作为一个逻辑是可定义的：命题连接词，如虚假，合取，析取，和功能空间，依赖功能空间，存在量化，平等，自然数，向量等。众所周知的类型的归约关系由此产生。为了进一步支持这个新的类型论的引入，我们还证明了它的项演算的基本性质。最重要的是，我们证明了主题减少和强规范化的减少关系，这使得计算意义的条款。所提出的类型论是基于第一作者以前研究过的分类逻辑的思想，它将Hagino的分类数据类型扩展到依赖类型化的设置。通过将类型论建立在范畴论的概念上，我们保持了归纳类型和上归纳类型之间的对偶性，并且它允许我们将函数空间描述为上归纳类型。
2016-05-07 cs.LO
Master Thesis Impredicative Encodings of Inductive and Coinductive Types
本硕士论文拓展Awodey等人的研究，在带扩展的λC系统中为System F风格归纳/共归纳类型构造满足（共）归纳原理的编码，覆盖列表、商、W-类型、流、M-类型等。
2025-05-15 cs.LO
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
守护递归是一种强大的模式递归方法，可以看作是步进索引的抽象形式。它目前被广泛用于分离逻辑，通过求解具有负出现的域方程来模拟具有高级功能的程序设计语言。在其多时钟版本中，保护递归也可以用于对共归纳类型进行编程和推理，编码类型中递归定义所需的生产力条件。本文提出了第一种类型论，它结合了多时钟保护递归和立方类型论的特点，并给出了一个指称语义。结合使用高阶归纳类型（Higher Inductive Types，HIT）和保护递归，可以对传统上难以在类型论中表示的共归纳类型进行简单的编程和推理，例如标记转移系统的分支分支类型。例如，我们的研究结果意味着这些双相似性意味着路径平等，因此证明可以沿着双相似性证明。我们的技术贡献之一是一个新的原则下的时钟感应。这允许在时钟上的通用量化与HIT交换直到等价的类型，并且对于共归纳类型的编码至关重要。这种交换性的要求已经制定了归纳类型的公理在以前的类型论与多时钟保护递归，但我们目前的配方作为一个归纳原则允许制定一般的计算规则。
2022-06-03 cs.LO
Higher inductive types in $(\infty,1)$-categories
本文在具有有限极限的$(\infty,1)$-范畴中定义高阶归纳类型，证明相关范畴有限可展示且初始对象存在，并证明初始对象的全局截面函子保持高阶归纳类型。
2024-10-23 cs.LO math.CT math.LO
Inductive Reasoning for Coinductive Types
本文提出 AlgCo 框架，利用代数完全偏序和稠密集合上的原始递归，实现对 conats、流等余归纳类型的归纳推理，并在 Coq 中验证了筛法、正则表达式库和概率采样语义。
2023-04-07 cs.LO
On Higher Inductive Types in Cubical Type Theory
立方类型论为同伦类型论的某些方面提供了一个建设性的证明，如Voevodsky的univalence公理。这使得许多外延性原则，如函数和命题外延性，可以在理论中直接证明。本文描述了一个构造性语义，表达在一个预层拓扑结构的适当结构的启发，立方集，一些更高的归纳类型。它还扩展了立方类型论的语法更高的归纳类型的领域，环面，悬浮液，截断，和推出。所有这些类型都由语义证明，并且对所有构造函数（包括高维构造函数）都有判断计算规则，并且在这些类型形成器下，宇宙是封闭的。
2018-04-30 cs.LO math.LO
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
本文将对偶演算推广为归纳型和余归纳型。本文首先介绍了一个非确定性的对偶演算的归纳和共归纳类型。它除了具有原对偶演算的对偶性外，还具有归纳型和余归纳型的对偶性，即归纳型和余归纳型的项和余项的对偶性及其归约规则的对偶性。它的强正规化也被证明，这是通过将其转化为一个二阶对偶演算。通过将二阶对偶演算转化为二阶对称λ演算，证明了二阶对偶演算的强正规化。本文接着介绍了归纳型和共归纳型对偶演算的按值调用系统和按名调用系统，并说明了按值调用和按名调用的对偶性、Church-Rosser性质和强规范性。通过将它们转化为具有归纳和共归纳类型的非确定性对偶演算，证明了它们的强规范化性。
2013-03-27 cs.LO cs.PL
Semantics for a Turing-complete Reversible Programming Language with Inductive Types
本文研究基于Theseus的高阶可逆编程语言，通过模式匹配保证函数可逆，证明其可编码任意可逆图灵机，构建了带模式匹配结构的并逆范畴语义，并证明其完全完备性，即可计算部分单射函数均为语言项的像。
2024-10-09 cs.LO
Two tricks to trivialize higher-indexed families
本文提出利用 Fording 和小宇宙索引两种技巧，将依赖类型论中具有高阶归纳索引的复杂索引族编码为无索引归纳类型与单一大型类型族，从而将其平凡化。
2023-10-30 cs.LO
Refining Inductive Types
依赖类型的程序设计语言允许在类型系统中表达数据的复杂属性。在依赖类型编程中特别有用的是索引类型，它通过计算上有用的信息来细化数据。例如，N索引类型的向量通过它们的长度来细化列表。其他数据类型也可以用类似的方式进行细化，但是程序员必须根据特定的目的进行细化，开发人员必须预测库中要包含哪些细化，并且实现必须经常存储有关数据及其细化的冗余信息。在本文中，我们将展示如何一般地推导归纳类型的细化归纳特征，并认为这些特征可以减轻一些与特设细化相关的上述困难。我们的特征也确保了标准的编程技术和推理归纳类型适用于细化，细化本身可以进一步细化。
2012-06-01 cs.LO cs.PL
The Calculus of Algebraic Constructions
本文讨论了代数构造演算（CAC）的基础，CAC是构造演算的归纳数据类型的扩展。CAC通过模式匹配提供函数的定义来概括配备高阶原始递归的归纳类型，该模式匹配捕获满足严格正性条件的任意非依赖和非多态归纳类型的递归定义。CAC还通过提供依赖类型和高阶重写规则来概括抽象数据类型的一阶框架。
2008-05-27 cs.LO
The Rooster and the Syntactic Bracket
我们提出了一个扩展的纯型系统的代数表示的诱导和共诱导型家庭适当的指标。这种类型论支持通过显式类型构造以及非谓词排序从较小的排序到较大的排序的扩展。非谓词排序中的类型族是用括号操作构造的。从非谓词排序到类型的模式匹配的必要限制仅限于括号结构。这种类型论给出了一个替代介绍归纳结构的演算上的Coq证明助手是一个实现。
2014-06-13 cs.LO
Higher Inductive Types as Homotopy-Initial Algebras
同伦类型论是基于马丁-洛夫构造性类型论和抽象同伦理论之间令人惊讶的和优雅的对应关系的一个新的数学领域。我们在这些学科之间有着强大的相互作用--我们可以使用几何直观来表述类型论中的新概念，相反，我们可以使用类型论的机器来验证并经常简化现有的数学证明。这个新系统中的一个关键成分是更高的归纳类型，它允许我们表示诸如球体、环面、推出物和平行物之类的对象。我们研究了一种高阶归纳类型的变体，它的计算行为取决于一个高阶路径，我们证明了在这种情况下，高阶归纳类型的特征在于它是一个同伦初始代数的泛性质.
2014-02-04 cs.LO math.CT math.LO
Functoriality of Enriched Data Types
Radboud University（拉德堡德大学）；Utrecht University（乌得勒支大学）；Michigan State University（密歇根州立大学）
本文研究了富足数据类型的 functorial 性，通过将自然变换纳入理论，扩展了诱导数据类型的定义，展示了如何将经典初始代数语义扩展到有限版本的数据类型。
2026-02-27 cs.LO math.CT
Inductive and Coinductive Components of Corecursive Functions in Coq
在构造类型论中，递归和上递归的定义受到语法限制，这保证了递归函数的终止性和上递归函数的生产力。然而，许多终止函数和生产函数没有通过语法测试。Bove在她的论文中提出了一个优雅的可访问性谓词方法的重新表述，该方法拓宽了构造类型论中可形式化的终结递归函数的范围。在本文中，我们追求同样的目标生产的上递归函数。值得注意的是，我们的方法的形式化coq生产函数的共归纳定义不仅需要使用特设谓词，而且还需要一个系统的算法，分离归纳和共归纳部分的功能。
2008-07-09 cs.LO
Global semantic typing for inductive and coinductive computing
归纳和共归纳类型通常被解释为本体（教会式）类型，表示规范的数据集，如自然数，列表和流。出于各种目的，特别是在全局语义上下文中研究程序，最好将类型视为语义属性（Curry风格）。内在理论是在20世纪90年代后期引入的，为程序及其语义类型的推理提供了一个纯粹的逻辑框架。在这里，我们将它们扩展到由归纳和共归纳定义的任何组合给出的数据。这种方法是有趣的，因为它与形式逻辑的语法，语义和证明理论基础紧密配合，在隐式计算复杂性以及从证明中提取程序方面具有潜在的应用。我们证明了一个规范性定理，表明程序类型的全球定义，通过通常的（塔斯基）语义的一阶逻辑，同意其操作语义在预期的模型。最后，我们表明，每一个内在的理论是一个保守的一阶算术扩展解释。这意味着对无限数据对象的量化本身不会导致证明理论的强度超过皮亚诺算术。内在理论完全服从于Curry-Howard态射公式，并被用来表征主要的计算复杂性类。
2014-12-24 cs.LO
Impredicative Encodings of (Higher) Inductive Types
本文针对依赖类型论中非直谓编码缺乏 η-等式和依赖消去的问题，提出基于同伦类型论的精化构造方法，并将其扩展至高阶归纳类型如 1-截断和单位圆 S1。
2018-02-08 cs.LO math.CT math.LO
Inductive types in homotopy type theory
同伦类型论（英语：Homotopy type theory）是马丁-勒夫的构造性类型论在抽象同伦理论中的一种解释。有结果之间的联系建设性数学和代数拓扑，提供拓扑语义内涵系统的类型理论，以及计算方法，代数拓扑通过类型理论为基础的证明助手，如Coq。目前的工作调查归纳类型在这种情况下。修改规则的归纳类型，包括类型的良基树，或W型，提出了，并确定了基本的同伦语义，这样的类型。所有结果的证明都已由Coq证明助理正式验证，并且用于此验证的证明脚本构成了本研究的重要组成部分。
2012-05-02 cs.LO math.CT math.LO
On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
本论文的目的是在同伦型理论的背景下提出综合同伦理论。我们将提出各种结果在这个框架中，最值得注意的是建设的Atiyah-Hirzebruch和塞尔谱序列的上同调，已完全正式的精益证明助手。
2018-08-31 cs.LO math.AT math.LO
Parametric Cubical Type Theory
我们展示了一个计算类型论，它结合了高维结构的carnivical立方类型论的内部参数化原语的参数类型论，绘制出两者之间的相似性和区别。结合理论既支持一价性，也支持它的关系等价物，我们称之为相对论。我们展示了使用的理论，通过分析多态类型，包括更高的归纳类型之间的功能，我们通过例子展示了如何相对性可以用来表征归纳类型的关系解释。
2019-07-08 cs.LO
Constructing Higher Inductive Types as Groupoid Quotients
本文在同伦类型论中证明所有有限一截断高阶归纳类型可由群胚商构造，定义签名及代数双范畴，并给出例子、极限与第一同构定理，形式化于Coq。
2021-04-21 cs.LO
Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
The University of Utah（犹他大学）
本文用立方阿格达形式化同调类型理论中的实数，避免了经典证明中的可数选择、 Bishop 集合构造的持久书务开销和 Dedekind 切割在预设类型理论中的繁琐层级跟踪。
2026-04-23 cs.LO
A topological reading of inductive and coinductive definitions in Dependent Type Theory
本文在依赖类型论中用共归纳生成的正性关系刻画共归纳谓词，并联系良基树的形式覆盖拓扑解释，全部证明已在 Agda 中形式化。
2024-04-04 cs.LO math.LO
Coinductive control of inductive data types
本研究结合归纳数据类型理论与通用测量理论，发现自函子代数范畴可在同自函子的余代数范畴中富集，该富集涵盖部分代数同态，还推广初始代数概念以定义新代数，丰富了代数范畴的信息。
2023-07-20 cs.LO math.CT
The Integers as a Higher Inductive Type
考虑了同伦类型论（HoTT）中整数的定义问题.我们可以将整数的类型定义为带符号的自然数（即，使用余积），但是它的归纳原理非常不方便使用，因为它导致了案例的爆炸。另一种方法是使用集合截断，但这里我们需要使用集合截断来避免非平凡的更高等式。这导致了一个递归原则，它只允许我们将函数定义为集合（满足UIP的类型）。在本文中，我们考虑使用小论域或双可逆映射的更高归纳类型。这些类型表示没有显式集截断的整数，等价于通常的余积表示。这是一个有趣的例子，因为它展示了如何在HoTT中处理一些一致性问题。我们讨论了这项工作引发的一些悬而未决的问题。证明已正式验证使用立方阿格达。
2020-07-01 cs.LO math.LO
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types
类型系统以组合的方式证明程序属性。从一个更大的程序中，可以抽象出一个部分，并通过使用被抽象出的部分的类型来证明所得到的抽象程序的属性。终止性和生产力是非平凡的，但所需的程序属性，并已提出了几个类型系统，保证终止，组成。这些类型系统与通过顺序迭代定义的最小和最大不动点密切相关。虽然大多数类型系统使用常规迭代，但我们在本文中考虑膨胀迭代。我们演示了这是如何导致一个更有原则的类型系统，递归基于有理有据的归纳。该类型系统有一个原型实现，MiniAgda，我们特别展示了它如何证明生产力的correcursive和混合递归correcursive功能。
2012-02-16 cs.LO cs.PL
Modular Composition of Inductive Types Using Lean Meta-programming
Qualgebra
本文提出基于元编程的归纳类型与函数实现组合算法及Lean语法扩展，实现模块化重用与扩展，并通过三子语言组合案例验证其特性与局限。
2026-09-23 cs.LO cs.PL cs.SE
Bootstrapping Inductive and Coinductive Types in HasCASL
我们讨论了处理的初始数据集和最终的进程类型的广谱语言HasCASL。特别是，我们提出的规范，说明了如何datatures和进程类型出现的自举概念，使用HasCASL的类型类机制，我们描述了有限和无限树的类型，建立保守性的datatype和进程类型声明坚持一定的合理格式的建设。后者相当于从HOL修改已知的结构，以避免唯一的选择;在分类术语，这意味着我们建立了拟对内部自然数对象支持初始代数和最终余代数的多项式函子的范围，从而部分概括相应的结果从拓扑理论。此外，我们提出了类似的建设范畴的内部完全偏序拟。
2008-12-25 cs.LO cs.SE
Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
程序设计语言中的归纳数据库允许用户定义有用的数据结构，如自然数、列表、树等。在本文中，我们将展示如何归纳数据库可以添加到量子程序设计语言QPL。我们构建了一个健全的分类模型的语言，并通过这样做，我们提供了第一个详细的语义处理用户定义的归纳数据在量子编程。我们还表明，我们的指称解释是不变的大步骤减少，从而建立另一个新的结果量子编程。与经典的编程相比，这个属性是相当困难的证明，我们展示了它的有用性，它如何立即意味着在所有类型的计算充分。为了进一步巩固我们的结果，我们的语义完全基于冯诺依曼代数的物理自然模型，冯诺依曼代数是物理学家用来研究量子力学的数学结构。
2019-10-21 cs.LO cs.PL math.CT
Cubical informal type theory: the higher groupoid structure
在同伦类型论一书中进行了一个为非正式类型论开发约定和符号的项目，该项目是为了建立一个框架，该框架是通过Voevodsky的univalance公理和更高的归纳类型来管理高维结构的公理来增强建设性类型论的，本文提出了一种以立方类型论为基础的非正式类型论的方法。为此，我们采用了一个立方体类型论最近提出的Angiuli，侯（Favonia）和哈珀，一个框架与累积层次的单价Kan宇宙，充分的univalence和实例的高归纳类型。本文只研究关于型的高广群结构的几个基本定理。
2018-06-22 cs.LO
Path Spaces of Higher Inductive Types in Homotopy Type Theory
等式类型的研究是同伦类型论的核心。描述这些类型通常很棘手，并且已经开发了各种策略，例如编码-解码方法。我们证明了一个定理的平等类型的coequalizers和pushout，让人想起一个归纳原则，没有任何限制的截断水平。这一结果使得有可能直接推理某些等式类型，并通过消除辅助结构的必要性来简化现有的证明。为了证明这一点，我们给出了一个很短的参数计算的基本群的圆（利卡塔和舒尔曼'13），并为事实，即推出保持嵌入。此外，我们的发展提出了一个更高版本的Seifert-van Kampen定理，并且集合截断算子将其映射到标准的Seifert-van Kampen定理（由于Favonia和Shulman '16）。我们提供了证明助理精益的主要技术成果的形式化。
2019-05-14 cs.LO math.LO
Complete Bidirectional Typing for the Calculus of Inductive Constructions
本文提出了一个归纳结构演算（CIC）的双向类型系统。它引入了一种介于通常的推理和检查之间的新判断，称为约束推理，以处理类型中的计算。该系统的关键属性是其相对于通常的无向系统的完备性，这已经在Coq中作为MetaCoq项目的一部分正式证明。虽然它在一个现实的类型化算法的持续完整性证明中扮演着重要的角色，但双向性的兴趣更广泛，因为它在试图证明CIC或设计变体和扩展的属性时提供了见解和结构。特别是，我们提出了约束推理，通常的推理和检查判断之间的中间，处理类型中的计算的存在。
2021-04-19 cs.LO cs.PL
Typed lambda-terms in categorical attributed graph transformation
本文讨论了基于属性图重写的模型转换。我们的贡献调查一个单一的推出方法应用重写规则。图的属性的计算是通过使用归纳类型的类型化演算来实现的。在本文中，我们提出了解决方案，以应付单推出建设的图形结构和计算功能。由于该重写系统使用归纳类型，属性计算的表达性得到了促进，并且比基于Sigma代数的重写系统更有效。本文描述了一些例子，显示我们的计算方法的兴趣。
2011-06-30 cs.LO
Totality for Mixed Inductive and Coinductive Types
本文提出带完全性检查器的混合归纳余归纳类型语言\chariot，通过奇偶博弈和大小变化原则确保递归定义终止，并已实现原型验证。
2025-09-02 cs.LO cs.PL
(Co)condition hits the Path
本文提出依赖类型理论中归纳类型与记录类型的（余）条件增强，推广了高阶归纳类型与路径类型，并展示了条件与余条件的对偶性及类型检查，但不涉及元理论。
2024-05-25 cs.LO cs.PL
Homotopies for Free!
我们显示“自由定理”的风格Wadler多态函数同伦类型论的抽象定理的后果。作为一个应用，它遵循每个定义为更高归纳类型的空间具有相同的同伦群作为某些类型的多态函数定义没有univalence或更高归纳类型。
2017-04-19 cs.LO math.LO
Solving Horn Clauses on Inductive Data Types Without Induction
基于归纳定义的数据结构，如列表和树，我们解决了约束Horn子句（CHC）的可满足性验证问题。我们提出了一种转换技术，其目标是删除这些数据结构的CHCs，从而减少其满足性的整数和布尔CHCs的可满足性问题。我们提出了一个转换算法，并确定了一类条款，它总是成功的。我们还考虑了该算法的扩展，它结合了子句转换与整数约束推理。通过实验评估，我们表明，我们的技术大大提高了Z3求解器的有效性，CHCs。我们还表明，我们的验证技术的基础上CHC转换，然后CHC解决方案，是有竞争力的CHC求解器与归纳扩展。本文件正在考虑被TPLP接受。
2018-04-24 cs.LO cs.PL
The equivalence of the torus and the product of two circles in homotopy type theory
同伦类型论是一个新的数学分支，它融合了抽象同伦论和高级范畴论与逻辑和类型论的观点。它允许我们将各种数学对象表示为基本类型论构造，更高的归纳类型。证明了在同伦类型论中，环面等价于两个圆的乘积。这一结果表明，环面作为高阶归纳型的综合定义是正确的。
2015-10-13 cs.LO math.LO
Formalising Inductive and Coinductive Containers
本文在Cubical Agda中形式化证明了容器保持最小与最大不动点，在不依赖UIP的条件下将容器函子理论从Set推广到类型的wild范畴，并展示了路径类型对共归纳证明的作用。
2025-07-04 cs.LO math.LO
Parametricity and Semi-Cubical Types
我们从一个任意的模型构造了一个具有参数性的类型论模型。新模型中的一个类型是旧模型中的半立方体类型，说明了参数性和立方体之间的对应关系。我们的结构不仅适用于参数性，而且适用于类型论的类似解释，实际上也适用于任何广义代数理论的类似解释。更准确地说，我们认为函子遗忘一元运算和方程定义他们递归的广义代数理论。证明了它有一个右伴随。我们使用的技术从局部可表示的范畴论，以及从商归纳归纳类型。
2022-01-25 cs.LO math.LO
