Guarded Cubical Type Theory: Path Equality for Guarded Recursion
本文将保护依赖类型论（GDTT）与立方类型论（CTT）相结合，改进了GDTT中等式的处理. GDTT是一种具有保护递归类型的可拓类型论，它对于建立程序逻辑模型以及使用共归纳类型进行程序设计和推理是有用的。我们希望用可判定的类型检查实现GDTT，同时仍然支持非平凡的等式证明，这是关于保护递归构造的扩展的原因。CTT是Martin-Löf类型论的变体，其中单位类型被项之间的抽象路径所取代。CTT提供了一个计算解释的功能扩展性，被证明有可判定的类型检查，并已实现的类型检查器。我们的新的类型论，称为守护立方类型论，提供了一个计算解释的可拓性守护递归类型。这进一步扩展了CTT作为数学和计算机科学形式化基础的基础。我们提出的例子来证明我们的类型论，所有这些都已经检查使用原型类型检查器实现的表达能力，并在一个preheaf类别的语义。
2016-06-28 cs.LO cs.PL
The clocks they are adjunctions:Denotational semantics for Clocked Type Theory
Clocked类型论（Clotted Type Theory，CloTT）是一种用于保护递归的类型论，可用于使用共归纳类型进行编程，允许将生产力编码在类型中，并用于使用步骤索引的抽象形式来推理高级程序设计语言功能。CloTT之前已经被证明具有许多语法属性，包括强规范化，规范性和类型检查的可判定性。在本文中，我们为CloTT提供了一个有用的指称语义，例如，用于研究未来的CloTT扩展，如路径类型。构建这个模型的主要挑战是对CloTT中用于共归纳类型的共归纳推理的滴答概念进行建模。我们建立在一个以前用于对保护递归进行建模的类别上，但是在这个类别中没有ticks对象，因此不能使用标准工具对上下文中的tick假设进行建模。相反，我们展示了如何使用伴随函子来建模滴答，以及如何使用语义替换来建模滴答常数。
2018-04-18 cs.LO
Using Structural Recursion for Corecursion
我们提出了一个（有限的）解决方案的问题，构造流值定义的递归方程，不尊重guardedness条件。在Coq、AGDA和其他高阶证明助手中，对上递归函数的定义施加了保护性条件。在本文中，我们特别集中在那些非守护方程递归调用下出现的功能。我们使用的流和函数之间的对应关系自然数表明，一些类的非保护的定义可以通过结构递归函数的编码建模。在实践中，这项工作扩展了流值类，可以在基于构造性类型论的定理证明器中定义归纳和共归纳类型，结构递归和保护共递归
2009-03-23 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
Dependent Inductive and Coinductive Types are Fibrational Dialgebras
在本文中，我建立了解释依赖归纳和共归纳类型所必需的范畴结构。众所周知，马丁-洛夫的依赖类型论可以使用纤维化来解释。然而，现代的定理证明器是基于更复杂的类型系统，允许定义强大的归纳依赖类型（称为归纳族）和有限的共归纳依赖类型。我定义了一类函子的纤维化，并显示如何数据类型定义对应于这些函子的初始和最终双代数。这种描述也是一种建议，即在类型论中应如何处理共归纳类型，因为它们在这里只是作为归纳类型的对偶出现。最后，我展示了依赖数据类型与代数和余代数的对应关系，并给出了依赖多项式函子的对应关系。
2015-09-10 cs.LO
Guarded Cubical Type Theory
本文将保护依赖类型论（GDTT）与立方类型论（CTT）相结合，改进了GDTT中等式的处理. GDTT是一种具有保护递归类型的可拓类型论，它对于建立程序逻辑模型以及使用共归纳类型进行程序设计和推理是有用的。我们希望用可判定的类型检查实现GDTT，同时仍然支持非平凡的等式证明，这些证明是关于保护递归构造的扩展的原因。CTT是Martin-Löf类型论的变体，其中单位类型被项之间的抽象路径所取代。CTT提供了一个计算解释的功能扩展性，享有规范的自然数类型，并被构造为支持可判定的类型检查。我们的新类型论，守护立方类型论（GCTT），提供了一个计算解释的可拓性守护递归类型。这进一步扩展了CTT作为数学和计算机科学形式化基础的基础。我们提出的例子来证明我们的类型论，所有这些都已检查使用原型类型检查器实现的表达能力。我们表明，CTT可以给出语义的立方体范畴和一个小的类别与初始对象的产品上的预层。然后，我们表明，类别的立方体类别和欧米茄的产品上的预层提供GCTT的语义。
2017-10-06 cs.LO math.CT math.LO
Context-Dependent Effects and Concurrency in Guarded Interaction Trees
IT University of Copenhagen（哥本哈根IT大学）；Univ Lyon, ENS de Lyon, UCBL, CNRS, Inria, LIP, UMR 5668, F-69342, Lyon CEDEX 07（里昂大学，里昂高等师范学校，里昂第一大学，法国国家科学研究中心，Inria，LIP实验室）；University of Groningen（格罗宁根大学）；Aarhus University（奥胡斯大学）
本文提出了一种扩展守卫交互树的方法，以支持依赖上下文的效果和抢占式并发的推理与表示。
2025-12-12 cs.LO cs.PL
Type Theory based on Dependent Inductive and Coinductive Types
我们开发了一个依赖的类型论，纯粹基于归纳和共归纳类型，以及相应的递归和共递归原则。这就产生了一个只有少量规则集的类型论，同时仍然具有相当的表达能力。例如，所有众所周知的基本类型和类型的形式，需要使用这个类型论作为一个逻辑是可定义的：命题连接词，如虚假，合取，析取，和功能空间，依赖功能空间，存在量化，平等，自然数，向量等。众所周知的类型的归约关系由此产生。为了进一步支持这个新的类型论的引入，我们还证明了它的项演算的基本性质。最重要的是，我们证明了主题减少和强规范化的减少关系，这使得计算意义的条款。所提出的类型论是基于第一作者以前研究过的分类逻辑的思想，它将Hagino的分类数据类型扩展到依赖类型化的设置。通过将类型论建立在范畴论的概念上，我们保持了归纳类型和上归纳类型之间的对偶性，并且它允许我们将函数空间描述为上归纳类型。
2016-05-07 cs.LO
A topological reading of inductive and coinductive definitions in Dependent Type Theory
本文在依赖类型论中用共归纳生成的正性关系刻画共归纳谓词，并联系良基树的形式覆盖拓扑解释，全部证明已在 Agda 中形式化。
2024-04-04 cs.LO math.LO
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
本文为时钟类型理论（CloTT）构建指称语义，利用依赖右伴随函子建模滴答概念，以支持余归纳推理，并改进了先前有缺陷且复杂的模型。
2020-12-14 cs.LO
Denotational semantics of recursive types in synthetic guarded domain theory
就像数学的任何其他分支一样，程序设计语言的指称语义应该在类型论中形式化，但是将传统的域理论语义（如最初在经典集合论中制定的）适应类型论已经证明是具有挑战性的。本文是一个项目的一部分，制定指称语义的类型论与保护递归。这样做的好处不仅是提供更简单的语义和充分性等属性的证明，而且有望在未来扩展到具有高级功能的语言，如通用引用，超出了传统域理论技术的范围。工作在保护依赖类型论（GDTT），我们开发的指称语义的FPC，简单类型的λ演算扩展与递归类型，建模的递归类型的FPC使用保护递归类型的GDTT。我们证明了GDTT模型的合理性和计算充分性，使用语法和语义之间的逻辑关系，也使用守护递归类型。指称语义是内涵的，在这个意义上，它计算计算一个项的值所需的展开-折叠约简的数量，但是我们构建了一个关系，该关系涉及外延相等项的指称，即，在不同步骤中计算相同值的项对。最后，我们展示了如何在类型论中执行术语的指称语义，并证明了执行布尔术语的指称计算与FPC的操作语义相同的值。
2018-05-02 cs.LO cs.PL
Guarded Computational Type Theory
中野后来的模态可以用来指定和定义递归函数，这些函数是因果或同步的;与时钟变量的概念相一致，也可以捕获更广泛的生产性（co）程序。到目前为止，很难将这些构造与依赖类型结合起来，以保持类型论的操作意义并承认宇宙的层次结构。我们提出了一个业务帐户的守卫依赖类型论与时钟称为守卫计算类型论，具有一个新的时钟交叉连接，享有时钟无关原则，以及谓词层次的宇宙，不需要任何索引的时钟上下文。守护计算类型论同时是一种具有丰富规范逻辑的程序设计语言，也是一种可用于开发其他语言和逻辑语义的计算元语言。
2018-04-24 cs.LO
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
我们提出的拓扑S的树作为一个模型的保护递归。我们研究了内部依赖类型的高阶逻辑的S，并表明S模型的两个模态算子，谓词和类型，作为后卫的递归定义的条款，谓词和类型。特别是，我们将展示如何解决递归类型方程涉及依赖类型。我们建议S的内部逻辑为程序设计语言和程序逻辑的步骤索引模型的抽象版本的合成构造提供了正确的设置。作为一个例子，我们展示了如何构建一个程序设计语言的模型，该语言具有完全在S内部逻辑中的高阶存储和递归类型。此外，我们给出了合成守护整环理论模型的公理化范畴处理，证明了对任何具有良基的完备Heyting代数A，A上层的拓扑构成合成守护整环理论的模型，推广了S的结果.
2012-10-01 cs.LO
Representing Continuous Functions between Greatest Fixed Points of Indexed Containers
本文提出用转换器表示余归纳类型间的可计算函数，推广了Hancock的工作，并在Agda中形式化，无需相等性但需归纳-递归定义。
2021-07-27 cs.LO
A constructive proof of dependent choice in classical arithmetic via memoization
在最近的一篇论文中，Herbelin开发了dPA ${^ω}$，这是一种微积分，其中可数和相关选择公理的构造性证明可以通过选择函数的记忆来推导。然而，规范化的属性（因此也是健全性的属性）只是被证明了。规范化证明的困难是由于同时存在依赖类型（对于选择的构造部分）、控制算子（对于经典逻辑）、共归纳对象（将${\mathbb{N} \to A}$类型的函数编码为流（${a_0},{a_1},...$））和共享的惰性求值（用于记忆这些共归纳对象）。阐述了以前的作品，我们在本文中介绍了一个变种的dPA ${^ω}$提出的一个微积分。一方面，我们利用Krivine经典可实现性的一个变体，我们开发了经典按需调用的规范化。另一方面，我们受益于dL ${_{\hat{tp}}}$，一个经典的依赖类型，其中类型安全性是通过使用定界的延续与语法限制一起确保演算。通过结合这些论文中开发的技术，我们设法定义了一个可实现性的解释我们的微积分，使我们能够证明规范化和健全。本文从Herbelin的dPA ${^ω}$开始，直到我们介绍它的dLPA ${^ω}$，对整个过程进行了回顾。
2019-03-18 cs.LO
A sequent calculus with dependent types for classical arithmetic
在最近的一篇论文中，Herbelin开发了一种演算dPA $^ω$，其中可数和依赖选择公理的构造性证明可以通过将可数全称量化的证明编码为一个组件流来推导。然而，规范化的属性（因此也是健全性的属性）只是被证明了。规范化证明的困难在于依赖依赖类型的同时存在（对于选择的建设性部分），控制运算符（用于经典逻辑），共归纳对象（将$N\rightarrow A$类型的函数编码为流$(a_0,a_1,\ldots)$）和具有共享的惰性求值（对于这些共归纳对象）。建立在以前的作品，我们在本文中介绍了一个变种的dPA $^ω$提出的一个微积分。一方面，我们利用我们开发的Krivine经典可实现性的一个变体来证明经典按需调用的规范化。另一方面，我们受益于dL，一个经典的依赖类型的微积分，其中类型安全是确保使用定界的延续与语法限制。通过结合这些文件中开发的技术，我们设法定义一个可实现的解释我们的微积分，使我们能够证明规范化和健全的。
2018-12-20 cs.LO
MiniAgda: Integrating Sized and Dependent Types
大小类型是一种模块化的、理论上易于理解的工具，用于检查递归的终止性和共递归定义的生产力。其基本思想是跟踪类型系统中的结构下降和保护性，以使终止检查健壮并适用于高阶函数和多态性等强抽象。为了研究大小类型在证明助手和基于依赖类型论的程序设计语言中的应用，我们实现了一个核心语言MiniAgda，它具有显式的大小处理。新的考虑是必要的，以合理地集成大小类型与依赖关系和模式匹配，这是可能的概念，如不可访问的模式和参数函数空间。本文提供了一个介绍MiniAgda的例子和非正式的解释的基本原则。
2010-12-22 cs.LO cs.PL
Denotational semantics of general store and polymorphism
本文首次提出结合卫递归与非直谓多态性的多态依赖类型理论指称语义，支持一般高阶引用和递归类型，并通过“逻辑关系即类型”的模态构造实现对有状态抽象数据类型的关系推理。
2023-04-12 cs.LO cs.PL
Sikkel: Multimode Simple Type Theory as an Agda Library
类型论的许多变体通过额外的原语或属性（如univalence，guarded recursion或parametricity）扩展了基本理论，以实现在原始理论中更难或不可能实现的构造或证明。然而，实现这种扩展的类型论（无论是从头开始还是通过修改现有的实现）是它们更广泛采用的一大障碍。在本文中，我们提出了Sikkel，在依赖类型的程序设计语言Agda，允许用户在扩展的类型论编程库。它使用了一种深度嵌入的语言，可以很容易地扩展额外的类型和术语构造函数，从而支持各种各样的类型论。此外，Sikkel有一个类型检查器，在这个意义上，所有类型良好的程序都自动转换为基于预层模型的浅嵌入中的语义。此外，我们的模型支持通过使用模态在它们之间传输定义来组合不同的基本类别。这使得特别是一个通用的方法提取定义的元级别，使我们可以使用扩展的类型论来定义定期Agda功能和证明他们的属性。在本文中，我们证明了Sikkel理论与保护递归和参数，但其他扩展可以很容易地插入。目前，Sikkel只支持简单的类型论，但它的模型已经预测了未来依赖类型和宇宙的增加。
2022-07-02 cs.LO cs.PL
Multimodal Dependent Type Theory
本文提出多模态依赖类型理论MTT，以模式理论为参数，统一保护递归、公理凝聚等模态情境，并证明其一致性与规范性。
2021-07-27 cs.LO
Modal Dependent Type Theory and Dependent Right Adjoints
近年来，我们已经看到了几个新的模型，依赖类型论扩展了某种形式的模态必要性算子，包括名义类型论，守卫和时钟类型论，空间和凝聚类型论。在本文中，我们研究模态依赖类型论：依赖类型论与运营商满足（依赖版本）的K公理的模态逻辑。我们研究语义和语法。对于语义，我们引入了具有依赖右伴随（Cwandom）的家族的类别，并表明上面的例子可以这样呈现。事实上，我们表明，任何有限的极限范畴的附加endofunctors引起的Cwerk通过当地的宇宙建设。对于语法，我们引入了一个依赖类型的扩展的Fitch风格的模态的Bunda演算，表明它可以在任何Cwetches解释，并建立一个长期的模型。我们扩展的语法和语义与宇宙。
2019-07-25 cs.LO
Non-Derivability Results in Polymorphic Dependent Type Theory
Radboud University Nijmegen（奈梅亨拉德堡德大学）；Eindhoven University of Technology（埃因霍温理工大学）；Institute for Computing and Information Science Faculty of Science（理学院计算与信息科学研究所）
本文研究了多形依赖类型理论中归纳原理和共归纳原理的可导性问题，发现参数quotient类型无法在λP2中定义，而流类型不具有共归纳原理，函数扩展性对归纳原理的可证明性至关重要。
2026-03-04 cs.LO math.LO
Transpension: The Right Adjoint to the Pi-type
本文提出transpension类型作为形状上全称量化的右伴随，给出类型规则与基于乘子的预层语义，并展示其与严格性公理结合可统一实现并改进多种现有内部化算子。
2024-06-18 cs.LO
