Type Theory based on Dependent Inductive and Coinductive Types
我们开发了一个依赖的类型论，纯粹基于归纳和共归纳类型，以及相应的递归和共递归原则。这就产生了一个只有少量规则集的类型论，同时仍然具有相当的表达能力。例如，所有众所周知的基本类型和类型的形式，需要使用这个类型论作为一个逻辑是可定义的：命题连接词，如虚假，合取，析取，和功能空间，依赖功能空间，存在量化，平等，自然数，向量等。众所周知的类型的归约关系由此产生。为了进一步支持这个新的类型论的引入，我们还证明了它的项演算的基本性质。最重要的是，我们证明了主题减少和强规范化的减少关系，这使得计算意义的条款。所提出的类型论是基于第一作者以前研究过的分类逻辑的思想，它将Hagino的分类数据类型扩展到依赖类型化的设置。通过将类型论建立在范畴论的概念上，我们保持了归纳类型和上归纳类型之间的对偶性，并且它允许我们将函数空间描述为上归纳类型。
2016-05-07 cs.LO
Inductive Reasoning for Coinductive Types
本文提出 AlgCo 框架，利用代数完全偏序和稠密集合上的原始递归，实现对 conats、流等余归纳类型的归纳推理，并在 Coq 中验证了筛法、正则表达式库和概率采样语义。
2023-04-07 cs.LO
Bisimulation as path type for guarded recursive types
在类型论中，共归纳类型用于表示进程，因此对于基于类型论的证明助手（如Coq和Agda）中的非终止反应式程序的形式化验证至关重要。目前，关于共归纳类型的编程和推理很困难，原因有两个：需要递归定义才能高效，以及内置标识类型和重要的双相似性概念缺乏重合。中野意义上的保护递归最近被认为是处理生产力问题的一种可能方法，允许将其编码在类型中。事实上，共归纳类型可以使用保护递归和时钟上的通用量化的组合来编码。本文研究了Ticked Cubical类型论中保护递归类型的双相似性概念，Ticked Cubical类型论是Cubical类型论的一个推广。我们证明了，对于任何函子，一个抽象的，范畴论的概念，双相似的最终守护余代数是等价的（在同伦类型论的意义上），以道路平等（原始概念的平等在立方类型论）。作为一个工作的例子，我们研究了一个守卫的概念标记的过渡系统，并表明，作为一个特殊的情况下的一般定理，路径平等符合适应通常的概念互模拟过程。特别是，这意味着保护递归可以用来给简单的等式推理证明的双相似性。这项工作应该被看作是使用上述编码获得双相似性作为共归纳类型的路径相等的一步。
2018-10-31 cs.LO
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
Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations
本文的目的是发展和研究共归纳谓词的递归证明。这样的递归证明允许人们在共归纳谓词的证明的构造中发现证明目标，同时仍然允许使用最高技术。这种方法解除了预先猜测不变量的负担，比如互模拟关系。相反，它们允许人们从追求的证明目标开始，并从那里发展证明，直到达到一个点，在这个点上，证明可以通过递归步骤关闭。以这种方式给出的证明更容易构造和理解，类似于循环证明系统或吸引人的参数化共归纳给出的证明。在本文中，我们开发了一个框架，递归证明的共归纳谓词，通过Fibrational谓词提升。这个框架是建立在所谓的后期模态，这已经使它出现在类型理论的设置之前。特别是，我们展示了递归证明的合理性和完整性，证明了兼容的最新技术可以用作递归证明中的推理规则，并提供了一些说明性例子。
2018-02-20 cs.LO
Dependent Inductive and Coinductive Types are Fibrational Dialgebras
在本文中，我建立了解释依赖归纳和共归纳类型所必需的范畴结构。众所周知，马丁-洛夫的依赖类型论可以使用纤维化来解释。然而，现代的定理证明器是基于更复杂的类型系统，允许定义强大的归纳依赖类型（称为归纳族）和有限的共归纳依赖类型。我定义了一类函子的纤维化，并显示如何数据类型定义对应于这些函子的初始和最终双代数。这种描述也是一种建议，即在类型论中应如何处理共归纳类型，因为它们在这里只是作为归纳类型的对偶出现。最后，我展示了依赖数据类型与代数和余代数的对应关系，并给出了依赖多项式函子的对应关系。
2015-09-10 cs.LO
Using Structural Recursion for Corecursion
我们提出了一个（有限的）解决方案的问题，构造流值定义的递归方程，不尊重guardedness条件。在Coq、AGDA和其他高阶证明助手中，对上递归函数的定义施加了保护性条件。在本文中，我们特别集中在那些非守护方程递归调用下出现的功能。我们使用的流和函数之间的对应关系自然数表明，一些类的非保护的定义可以通过结构递归函数的编码建模。在实践中，这项工作扩展了流值类，可以在基于构造性类型论的定理证明器中定义归纳和共归纳类型，结构递归和保护共递归
2009-03-23 cs.LO
Denotational semantics for guarded dependent type theory
我们提出了一个新的模型的保护依赖类型论（GDTT），一个类型论与保护递归和多个时钟，其中一个可以编程，共归纳类型的原因。递归定义的共归纳程序和证明的生产力是使用保护递归编码在类型中的，因此可以模块化地检查，不像现代证明助手中实现的语法检查。该模型基于一类时间对象的协变预层，并使用时钟的预层对时钟进行量化建模。为了模拟时钟无关性公理，这对于使用共归纳类型进行编程至关重要，类型必须被解释为与时钟对象正交的预层。在依赖类型的情况下，这转化为提升条件，类似于在类型论的同伦理论模型中发现的提升条件，但在这里具有提升唯一性的额外要求。由于在这个模型中标准的Hofmann-Streicher构造定义的宇宙不满足这个性质，GDTT中的宇宙必须通过时钟变量的上下文来索引。我们展示了如何模拟这些宇宙的方式，时钟上下文的夹杂物引起的夹杂物的宇宙与类型操作的鼻子。
2020-04-13 cs.LO
The Size-Change Principle for Mixed Inductive and Coinductive types
本文针对嵌套归纳与余归纳类型，改进大小变化原理以检查递归定义的完全性，确保其相对于相应类型的正确性。
2025-09-02 cs.LO
Master Thesis Impredicative Encodings of Inductive and Coinductive Types
本硕士论文拓展Awodey等人的研究，在带扩展的λC系统中为System F风格归纳/共归纳类型构造满足（共）归纳原理的编码，覆盖列表、商、W-类型、流、M-类型等。
2025-05-15 cs.LO
Coinductive Formal Reasoning in Exact Real Arithmetic
在这篇文章中，我们提出了一种方法，正式证明的正确性懒惰算法计算单应性和二次变换-字段操作的特殊情况下-由共归纳流的实数表示。该算法工作在Möbius映射的共归纳流上，并形成了Edalat-Potts精确实算术的基础。我们使用Coq的证明助手的机器来表示共归纳类型的形式化。形式化的算法只是部分生产性的，即，它们并不为所有可能的输入输出可证明的无限流。我们将展示如何处理这一问题的句法限制的存在所造成的建设性类型论的Coq。此外，我们表明，我们开发的类型理论技术是兼容的语义的算法作为连续映射实数。由此产生的Coq形式化可供公众下载。
2008-09-10 cs.LO
Inductive and Coinductive Components of Corecursive Functions in Coq
在构造类型论中，递归和上递归的定义受到语法限制，这保证了递归函数的终止性和上递归函数的生产力。然而，许多终止函数和生产函数没有通过语法测试。Bove在她的论文中提出了一个优雅的可访问性谓词方法的重新表述，该方法拓宽了构造类型论中可形式化的终结递归函数的范围。在本文中，我们追求同样的目标生产的上递归函数。值得注意的是，我们的方法的形式化coq生产函数的共归纳定义不仅需要使用特设谓词，而且还需要一个系统的算法，分离归纳和共归纳部分的功能。
2008-07-09 cs.LO
An operational interpretation of coinductive types
本文为严格正嵌套高阶（余）归纳类型提出一种基于重写的操作语义，通过逼近定理证明良类型项具有良好定义的解释，推广了生产力概念。
2020-02-12 cs.LO
Structured general corecursion and coinductive graphs [extended abstract]
Bove和Capretta用一般递归方程来证明函数定义的流行方法是基于这样的观察：任何结构化的一般递归方程定义了一个预期域（“定义域”）的归纳子集，该方程具有唯一的解。要接受这个定义，只要证明这个子集包含整个预定域就足够了。这种方法对于“终止”定义非常有效。但是它没有考虑到“生产性”的定义，例如流值函数的典型定义。我们认为，这样的定义可以被视为在一个类似的精神，从一个不同的独特的可解性标准。任何结构化的递归方程都定义了预定域和预定余域之间的共归纳关系（“共归纳图”）。这个关系又确定了一个子集的预期域和商的预期的余域的属性，该方程是唯一解决的子集和商。因此，只要子集是全集且商是相等的，就保证方程对于预定域和预定余域有唯一解。
2012-02-16 cs.LO cs.PL
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types
类型系统以组合的方式证明程序属性。从一个更大的程序中，可以抽象出一个部分，并通过使用被抽象出的部分的类型来证明所得到的抽象程序的属性。终止性和生产力是非平凡的，但所需的程序属性，并已提出了几个类型系统，保证终止，组成。这些类型系统与通过顺序迭代定义的最小和最大不动点密切相关。虽然大多数类型系统使用常规迭代，但我们在本文中考虑膨胀迭代。我们演示了这是如何导致一个更有原则的类型系统，递归基于有理有据的归纳。该类型系统有一个原型实现，MiniAgda，我们特别展示了它如何证明生产力的correcursive和混合递归correcursive功能。
2012-02-16 cs.LO cs.PL
Mechanizing Coinduction and Corecursion in Higher-order Logic
递归和上递归定义的理论已经在高阶逻辑（HOL）中得到了发展，并使用Isabelle进行了机械化。最小不动点表示归纳数据类型，如严格列表;最大不动点表示共归纳数据类型，如懒惰列表。良基递归表示归纳数据类型上的递归函数;协递归表示产生共归纳数据类型元素的函数。该理论依赖于传统的形式化的无限树。该理论旨在用于规范和验证。它支持大范围的可计算函数的推理，但没有形式化它们的操作语义，也可以表示不可计算函数。该理论说明使用有限和无限的列表。共递归表示无限列表上的函数;共归纳推理这类函数。
2000-10-31 cs.LO
From coinductive proofs to exact real arithmetic: theory and applications
基于连续函数的一个新的共归纳特征，我们从构造性证明中提取了精确实数计算的认证程序。提取的程序构造和组合精确的实数算法相对于实数的二进制有符号数字表示。对应于连续函数的共归纳定义的数据类型由描述算法何时写入和读取数字的非良基树组成。我们讨论了几个例子，包括提取多项式的程序，直到二次和连续映射的定积分。
2012-04-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
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
本文将对偶演算推广为归纳型和余归纳型。本文首先介绍了一个非确定性的对偶演算的归纳和共归纳类型。它除了具有原对偶演算的对偶性外，还具有归纳型和余归纳型的对偶性，即归纳型和余归纳型的项和余项的对偶性及其归约规则的对偶性。它的强正规化也被证明，这是通过将其转化为一个二阶对偶演算。通过将二阶对偶演算转化为二阶对称λ演算，证明了二阶对偶演算的强正规化。本文接着介绍了归纳型和共归纳型对偶演算的按值调用系统和按名调用系统，并说明了按值调用和按名调用的对偶性、Church-Rosser性质和强规范性。通过将它们转化为具有归纳和共归纳类型的非确定性对偶演算，证明了它们的强规范化性。
2013-03-27 cs.LO cs.PL
Global semantic typing for inductive and coinductive computing
归纳和共归纳类型通常被解释为本体（教会式）类型，表示规范的数据集，如自然数，列表和流。出于各种目的，特别是在全局语义上下文中研究程序，最好将类型视为语义属性（Curry风格）。内在理论是在20世纪90年代后期引入的，为程序及其语义类型的推理提供了一个纯粹的逻辑框架。在这里，我们将它们扩展到由归纳和共归纳定义的任何组合给出的数据。这种方法是有趣的，因为它与形式逻辑的语法，语义和证明理论基础紧密配合，在隐式计算复杂性以及从证明中提取程序方面具有潜在的应用。我们证明了一个规范性定理，表明程序类型的全球定义，通过通常的（塔斯基）语义的一阶逻辑，同意其操作语义在预期的模型。最后，我们表明，每一个内在的理论是一个保守的一阶算术扩展解释。这意味着对无限数据对象的量化本身不会导致证明理论的强度超过皮亚诺算术。内在理论完全服从于Curry-Howard态射公式，并被用来表征主要的计算复杂性类。
2014-12-24 cs.LO
Guarded Dependent Type Theory with Coinductive Types
我们提出了守护依赖类型论，gDTT，一个扩展的依赖类型论与“后来”的模态和时钟量词的编程和证明与守护递归和共归纳类型。后一种模态用于以模块化的、基于类型的方式确保递归定义的生产力。时钟量词用于控制消除后一种模态，并使用保护递归类型对共归纳类型进行编码。发展gDTT的关键是新型和术语形成者，涉及我们所说的“延迟替代”。这些概括了早期工作中考虑的后一种模态的适用函子规则，并且对于依赖类型的编程和证明至关重要。我们证明了相对于指称模型的类型论的合理性。
2016-01-07 cs.LO cs.PL
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
Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas
在最近的工作中，我们已经展示了如何通过将程序抽象编译成Horn公式f来为面向对象语言定义非常精确的类型系统。那么类型推断就等于解决了一个特定的目标。f的共归纳（也就是最大的）Herbrand模型。以这种方式定义的类型系统是理想化的，因为在最有趣的实例化中，共同归纳的Herbrand论域和目标导子的项都不能被直接表示。然而，声音和相当有表现力的近似可以通过只考虑正则项和导数来实现。在这样做的时候，引入一个适当的子类型关系来形式化类型之间近似的概念是至关重要的。本文研究了建立在联合和对象类型构造函数上的共归纳项的子类型关系。我们定义了一个解释的类型作为一组值引起的一个相当直观的关系的成员资格的值类型，并证明了子类型的定义是健全的w.r.t.类型解释之间的子集包含。可靠性的证明使我们能够简化压缩派生的概念，并发现先前给出的子类型定义并没有涵盖空类型的所有可能表示。
2010-06-08 cs.LO cs.PL
Formalising Inductive and Coinductive Containers
本文在Cubical Agda中形式化证明了容器保持最小与最大不动点，在不依赖UIP的条件下将容器函子理论从Set推广到类型的wild范畴，并展示了路径类型对共归纳证明的作用。
2025-07-04 cs.LO math.LO
Coinductive control of inductive data types
本研究结合归纳数据类型理论与通用测量理论，发现自函子代数范畴可在同自函子的余代数范畴中富集，该富集涵盖部分代数同态，还推广初始代数概念以定义新代数，丰富了代数范畴的信息。
2023-07-20 cs.LO math.CT
Bootstrapping Inductive and Coinductive Types in HasCASL
我们讨论了处理的初始数据集和最终的进程类型的广谱语言HasCASL。特别是，我们提出的规范，说明了如何datatures和进程类型出现的自举概念，使用HasCASL的类型类机制，我们描述了有限和无限树的类型，建立保守性的datatype和进程类型声明坚持一定的合理格式的建设。后者相当于从HOL修改已知的结构，以避免唯一的选择;在分类术语，这意味着我们建立了拟对内部自然数对象支持初始代数和最终余代数的多项式函子的范围，从而部分概括相应的结果从拓扑理论。此外，我们提出了类似的建设范畴的内部完全偏序拟。
2008-12-25 cs.LO cs.SE
Non-wellfounded trees in Homotopy Type Theory
我们证明了同伦类型论中关于共归纳类型的可构造性的一个猜想--以索引M-类型的原则形式。该猜想说，在归纳类型存在的情况下，共归纳类型是可导出的。事实上，在这项工作中，我们在同伦类型论的一个子系统中构造了共归纳类型;这个子系统由内涵马丁-洛夫类型论与自然数和Voevodsky的单价公理给出。我们的结果在计算机证明助手Agda中实现了机械化。
2015-04-12 cs.LO math.CT
Representing Continuous Functions between Greatest Fixed Points of Indexed Containers
本文提出用转换器表示余归纳类型间的可计算函数，推广了Hancock的工作，并在Agda中形式化，无需相等性但需归纳-递归定义。
2021-07-27 cs.LO
Totality for Mixed Inductive and Coinductive Types
本文提出带完全性检查器的混合归纳余归纳类型语言\chariot，通过奇偶博弈和大小变化原则确保递归定义终止，并已实现原型验证。
2025-09-02 cs.LO cs.PL
Flexible Coinduction in Agda
定理证明器是帮助用户编写机器可读证明的工具。其中一些工具也是交互式的。对这种软件的需求正在增加，因为它们提供的证明比手写的证明更可靠。Agda基于类型论和命题作为类型的对应关系，具有类似Haskell的语法。这意味着一个声明的证明被转换成一个函数。推理系统是定义归纳和共归纳谓词的一种方式，归纳和共归纳原则被提供来帮助证明它们在可靠性和完整性方面相对于给定规范的正确性。广义推理系统处理的谓词的归纳和共归纳的解释不提供预期的判断集。在这种情况下，推理系统被证明树中可以无限深度应用的规则所丰富。归纳和共归纳原理不能用于广义推理系统的情况下，有界共归纳原理已被提出。我们首先介绍了Agda如何支持归纳和共归纳类型，强调了数据结构和谓词是使用相同的构造定义的这一事实。然后，我们转移到这篇论文的主题，这是研究如何广义推理系统可以实现和如何证明他们的正确性。
2020-02-17 cs.LO
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
Type-Based Termination for Futures
本文将顺序语言中的大小类型终止性检查方法适配到并发场景，通过扩展半公理化相继式演算提出大小类型细化方案，借助无限宽有限深的类型推导树和新颖逻辑关系论证，实现基于futures的函数式并发程序的终止性验证。
2024-04-15 cs.LO cs.PL
Constructing Recursion Operators in Intuitionistic Type Theory
马丁-勒夫的直觉主义类型理论在计算机程序的形式化推理中越来越流行。为了处理递归计划以外的原始递归，良基关系的理论。使用原始递归在更高的类型，归纳和递归正式推导出一个大类的良好的基础关系。包括<自然数，和关系形成的逆图像，加法，乘法，和指数的其他关系。构造给出了充分的细节，让他们使用的定理证明类型论，如Nuprl。该理论的工作相比，在该领域的有序递归更高的类型。
2000-10-31 cs.LO
Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency
我们定义了一个π演算的变种与成本语义通道被视为资源，必须明确分配之前，他们被使用，可以被释放时不再需要。我们使用一个子结构类型系统跟踪权限转移构造共归纳证明技术比较行为和资源使用效率的并发进程。我们建立我们的共归纳定义和上下文行为前序描述的概念，过程效率w.r.t.之间的充分抽象的结果。它的资源管理。我们还证明了这些定义和相应的证明技术，通过大量的例子和案例研究比较两个并发实现的可扩展缓冲区。
2014-06-24 cs.LO
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types
在本文中，我们提出了一个简单类型的lambda项的规范化的Agda形式化。正规化器由两个在延迟单子中共归纳定义的函数组成：一个是闭包的lambda项的标准求值器，另一个是从值到η-long beta-范式的类型定向具体化器。他们的组成，规范化的评价，被证明是一个总功能的后验，使用标准的逻辑关系参数。成功的形式化作为一个概念的证明共归纳编程和推理使用大小类型和copatteries，一个新的和目前的实验功能的Agda。
2014-06-09 cs.LO cs.PL
Type homogeneity is not a restriction for safe recursion schemes
Knapik等人引入了安全约束，它约束了定义高阶递归方案的产生式规则的类型和语法。这种限制会导致一个equi-expressivity的结果之间的阶n下推自动机和阶n安全递归计划，当这样的设备被用作树生成器。我们表明，类型的安全约束，称为同质性，是不必要的，在这个意义上说，单独施加的句法限制是足以证明树的等表现力的结果。
2017-01-09 cs.LO
Time-complexity semantics for feasible affine recursions (extended abstract)
作者的ATR编程形式主义是复杂性理论驱动的类型系统下的按值调用PCF的一个版本。ATR程序运行在2型多项式时间内，所有标准的2型基本可行泛函都是ATR可定义的（ATR类型被限制在0、1和2级）。原始版本的ATR的一个局限性是，唯一可直接表达的递归是尾递归。在这里，我们扩展ATR，使广泛的仿射递归直接表达。特别是，修改后的ATR可以相当自然地表达经典的插入和选择排序算法，从而克服了大多数以前的隐复杂性为基础的形式主义的症结。本文的主要工作是在扩展和简化原来的ATR的时间复杂度语义，开发一套工具，用于提取和解决所产生的高类型的递归可行的仿射递归。
2007-03-20 cs.LO
Recursion does not always help
该研究表明，在类型化 λβη-演算和 λΩ-演算中加入递归不会增加可定义的全函数或偏函数，并由此得出自由代数及自然数上的可定义函数类别也不会扩大。
2023-07-18 cs.LO
Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
我们提出了第一个会话类型系统，保证可能非终止通信进程的请求-响应活性属性。这些类型用一组所需的响应来扩充标准二进制会话类型的分支和选择类型，这表明每当选择特定标签时，最终也必须选择一组其他标签，即其响应。我们证明，这些扩展类型是严格的表达比标准的会话类型。我们提供了一个类型系统的过程演算类似于一个子集的内部（基于数据）和外部（基于事件）分支，消息传递，有界和无界循环的协作BPMN流程。我们证明了这个类型系统是合理的，即，它保证了无死锁进程的请求-响应活性。我们在一个无限状态系统的具体例子上说明了微积分和类型系统的使用。
2016-01-05 cs.LO
Type Inference for Bimorphic Recursion
本文提出了双态递归，这是一种受限制的多态递归，使得函数定义体中的每个递归调用具有相同的类型。双态递归允许我们为递归定义的函数分配两种不同的类型：一种是递归调用，另一种是定义之外的调用。本文中的双态递归是可以嵌套的。本文证明了双态递归具有主类型和可判定的类型推断。因此，双态递归给我们提供了灵活的递归类型和可判定的类型推断。本文还表明，它的类型成为不可判定的，因为嵌套的递归时，从双态递归删除的实例化属性。
2011-06-07 cs.LO cs.PL
Taking a Detour to Zero: An Alternative Formalization of Functions Beyond PR
有两个著名的系统形式化超越原始递归的全递归（\textbf{PR}），Gödel的系统\textbf{T}和Girard和Reynolds的系统\textbf{F}。系统\textbf{T}定义了类型化对象的递归，并能构造Heyting算法（\textbf{HA}）的各个函数。系统\textbf{F}引入了类型变量，可以定义系统\textbf{T}的递归。其结果是一个系统的表达作为二阶海廷算法（\textbf{HA} $_{2}$）。虽然，两者都能够表达不可否认的快速增长的功能，在某些应用中，需要更灵活的形式主义。一个这样的应用程序是CERES削减消除示意性\textbf{LK} -证明（$CERES_{s}$），其中递归的形状是重要的。在本文中，我们介绍了快速增长的功能没有类型论基础的形式主义。递归由自然数的有序集合索引。我们强调了我们的递归和Winer层次结构之间的关系，以提供与现有系统的比较。我们可以证明，我们的形式表示的功能表示使用系统\textbf{T}。我们将系统\textbf{F}和以后的工作进行比较。
2018-01-03 cs.LO
The recursion hierarchy for PCF is strict
本文证明PCF语言中，按类型层级限制不动点算子会形成严格层级，即高层级的不动点算子无法用低层级定义，并利用嵌套顺序过程理论解答了Berger的问题。
2018-08-20 cs.LO
Unboundedness for Recursion Schemes: A Simpler Type System
无界性和同时无界性问题的可判定性（又名。高阶递归格式的对角问题）由Clemente，Parys，Salvati和Walukiewicz（2016）建立。然后Parys（2017）提出了一个最佳复杂度的过程;这个过程使用了一个复杂的类型系统，涉及多个标志和标记。我们在这里提出了一个更简单和更直观的类型系统服务于相同的目的。我们证明，这种类型的系统允许解决无界性问题的递归计划，被广泛认为是一个子类，称为安全的计划。对于不安全的递归模式，我们只有类型系统的可靠性：如果一个人可以建立一个类型派生，声称递归模式是无界的，那么它确实是无界的。不安全递归模式的类型系统的完整性是一个悬而未决的问题。更进一步，我们讨论了类型系统的扩展，允许处理同时无界性问题。我们还设计并实现了一种算法，可以完全自动检查给定递归方案的无界性，并在短时间内完成各种输入。
2022-04-23 cs.FL cs.LO
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
本文在守护类型论中利用高阶归纳类型和守护递归建模带概率选择与递归类型的语言，并建立操作与指称语义间的关系以支持充分性和上下文等价推理。
2024-10-24 cs.LO cs.PL
A Generalized Modality for Recursion
中野的后期模态允许类型表示函数的输出不直接依赖于其输入，因此计算其不动点是安全的。事实证明，这种保护递归的想法在各种上下文中都很有用，从具有无限数据结构的函数式编程到类型论内部的步进索引公式。分类模型表明，后一种模态本质上对应于离散时间尺度的简单重新索引。不幸的是，现有的保护类型论遭受编程目的的重大限制。这些局限性源于这样一个事实，即后一种模态的表达能力不足以捕捉函数的精确输入-输出依赖关系。因此，守卫类型论拒绝许多生产性定义。结合守卫类型论和同步程序设计语言的见解，我们提出了一个新的模式守卫递归。此模态可以将时间尺度的任何行为良好的重新索引应用于类型。我们称这种重新索引为时间扭曲。文献中的几种模态，包括后来的模态，对应于固定的时间扭曲，因此作为我们的特例出现。
2020-08-03 cs.LO cs.PL
Intensionality, Intensional Recursion, and the Gödel-Löb axiom
在类型化的$λ$演算中使用必要性模态可以将其分成两个区域。这些可以被认为是内涵与外延数据：第一个区域中的数据，模态数据，可以作为代码使用，并且可以检查它们的描述。相比之下，第二区域中的数据仅可用作达到普通相等的值。这允许我们在模态类型上添加非函数操作，同时保持一致性。在这种情况下，哥德尔-洛布公理获得了一种新颖的建设性解读：它为程序员提供了一种非常强的递归的可能性，使他们能够编写能够访问自己代码的程序。这是一种计算反射，强烈地让人想起Kleene的第二递归定理。
2020-06-13 cs.LO cs.PL
Ramified Structural Recursion and Corecursion
我们调查可行的计算在一个相当一般的概念的数据和codata。具体来说，我们提出了一个直接Bellantoni库克风格的正常/安全类型的编程形式主义，RS 1，表示可行的结构递归和corerursions的数据和codata指定的多项式函子。（列表、流、有限树、无限树等都是可以直接定义的。RS 1的一个新颖之处在于它像标准函数式编程实现一样包含了结构共享。由于我们的数据表示使用共享，我们的结构递归的实现是memoized，以避免可能的指数，许多重复的子计算一个天真的实现可能执行。我们引入的概念表示的数据（占共享）和codata（使用的想法类型2计算复杂性）的大小，并建立类型级别1 RS 1函数具有多项式有界的运行时，并满足多项式时间的完整性条件。此外，将RS 1项限制为特定类型会产生一些标准复杂度类的特征（例如，Ω-正则语言，线性空间函数）和一些不太标准的类（例如，日志空间流）。
2012-01-27 cs.LO cs.PL
A Light Modality for Recursion
本文提出一种语法上静默的模态，用于控制无限结构上递归函数式程序的行为，将递归控制负担从程序员转移到编译器，并引入带静默模态和守护递归类型的类型化lambda演算，保证归一化且可推断类型。
2019-02-02 cs.LO cs.PL
Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction
我们通过构造性类型论的眼镜来看待具有交互式I/O的语言的操作语义。从我们早期的工作，基于共归纳跟踪的语义虽然，我们定义了几个大步骤的语义，而与交互式I/O，基于删除和终止敏感的弱双相似性。这需要在共归纳定义中嵌套归纳定义，这在数学上和在证明助手中实现的观点上都是有趣的。在第一次定义了一个基本的语义的声明中明确的内部动作（延迟）的delictions，我们引入了一个语义的无延迟delictions，基本上消除了有限的延迟序列的飞行从这些delictions是响应。最后，我们还研究了一个语义方面的无延迟的附加选项，一个沉默的分歧选项。这种语义取决于收敛和发散之间的决定，并且只等价于经典的基本语义。我们已经完全正式化了我们在Coq的发展。
2010-08-12 cs.LO cs.PL
Two algorithms in search of a type system
作者的ATR编程形式主义是复杂性理论驱动的类型系统下的按值调用PCF的一个版本。ATR程序运行在2型多项式时间内，所有标准的2型基本可行泛函都是ATR可定义的（ATR类型被限制在0、1和2级）。原始版本的ATR的一个局限性是，唯一可直接表达的递归是尾递归。在这里，我们扩展ATR，使广泛的仿射递归直接表达。特别是，修改后的ATR可以相当自然地表达经典的插入和选择排序算法，从而克服了大多数以前的隐复杂性为基础的形式主义的症结。本文的主要工作是在提炼原来的时间复杂度语义ATR表明，这些新的递归计划不会导致的可行性领域。
2008-04-18 cs.LO cs.PL
Efficient Type Checking for Path Polymorphism
一个类型系统组合类型应用，常量类型，联合类型（关联，交换和幂等）和递归类型最近已被提出的静态类型路径多态性，能够定义函数，可以统一操作递归指定的应用数据结构。这样的函数所采用的典型模式是$x\,y$，它将一个复合物（换句话说，任何适用的树结构）分解成它的部分。我们分两个阶段来研究这个类型系统的类型检查。首先，我们提出了算法检查类型等价和子类型的基础上，这些关系的共归纳特征。然后，我们制定了一个语法导向的演示文稿，并证明其与原来的等价。这产生了一个类型检查算法，不幸的是，在最坏的情况下，它具有指数级的时间复杂度。第二个算法，然后提出，自动机技术的基础上，产生一个多项式时间的类型检查算法。
2017-04-28 cs.LO cs.PL
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
