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
Type Inference for Guarded Recursive Data Types
我们考虑保护递归数据类型（GRDT）的类型推断--代数数据类型的最新概括。我们减少类型推断GRDTs统一下的混合前缀。因此，我们得到有效的类型推断。推断是不完整的，因为允许出现在类型系统中的类型约束集只是由类型推断生成的那些类型约束的子集。因此，只有当程序被充分地类型注释时，推理才会成功。我们提出了完善的程序，逐步推断类型，并协助用户识别哪些类型的信息丢失。此外，我们还引入了一些过程来测试一个类型是否不是主体类型，并在存在主体类型时查找主体类型。
2005-07-14 cs.LO cs.PL
Denotational semantics of recursive types in synthetic guarded domain theory
就像数学的任何其他分支一样，程序设计语言的指称语义应该在类型论中形式化，但是将传统的域理论语义（如最初在经典集合论中制定的）适应类型论已经证明是具有挑战性的。本文是一个项目的一部分，制定指称语义的类型论与保护递归。这样做的好处不仅是提供更简单的语义和充分性等属性的证明，而且有望在未来扩展到具有高级功能的语言，如通用引用，超出了传统域理论技术的范围。工作在保护依赖类型论（GDTT），我们开发的指称语义的FPC，简单类型的λ演算扩展与递归类型，建模的递归类型的FPC使用保护递归类型的GDTT。我们证明了GDTT模型的合理性和计算充分性，使用语法和语义之间的逻辑关系，也使用守护递归类型。指称语义是内涵的，在这个意义上，它计算计算一个项的值所需的展开-折叠约简的数量，但是我们构建了一个关系，该关系涉及外延相等项的指称，即，在不同步骤中计算相同值的项对。最后，我们展示了如何在类型论中执行术语的指称语义，并证明了执行布尔术语的指称计算与FPC的操作语义相同的值。
2018-05-02 cs.LO cs.PL
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。
2016-09-05 cs.LO cs.PL
Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。
2015-01-15 cs.LO cs.PL
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
Guarded Dependent Type Theory with Coinductive Types
我们提出了守护依赖类型论，gDTT，一个扩展的依赖类型论与“后来”的模态和时钟量词的编程和证明与守护递归和共归纳类型。后一种模态用于以模块化的、基于类型的方式确保递归定义的生产力。时钟量词用于控制消除后一种模态，并使用保护递归类型对共归纳类型进行编码。发展gDTT的关键是新型和术语形成者，涉及我们所说的“延迟替代”。这些概括了早期工作中考虑的后一种模态的适用函子规则，并且对于依赖类型的编程和证明至关重要。我们证明了相对于指称模型的类型论的合理性。
2016-01-07 cs.LO cs.PL
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
Garlene: Guarded Recursion in Lean
IT University of Copenhagen（哥本哈根信息技术大学）；Aarhus University（奥胡斯大学）
本文提出 Garlene，一种在 Lean 中实现保护递归的嵌入式语言，提供直观语法与专用证明模式，并通过预层模型证明其可靠性，支持导出至标准 Lean 开发，以解决主流定理证明器缺乏保护递归支持的问题。
2026-09-22 cs.LO cs.PL
Beating the Productivity Checker Using Embedded Languages
一些全语言，如Agda和Coq，允许使用保护上递归来构造无穷值和证明。保护共递归（英语：Guarded corecursion）是递归的一种形式，其中允许任意递归调用，只要它们被共归纳构造函数保护。守护性确保程序是生产性的，即可以在有限时间内计算无限值的每个有限前缀。然而，许多生产性程序不是受保护的，并且将它们置于受保护的形式中可能是不平凡的。本文给出了一种将生产性程序转化为防护程序的方法。该方法相当于将特定于问题的语言定义为数据类型，用特定于问题的语言编写程序，并为该语言编写一个受保护的解释器。
2010-12-22 cs.LO cs.PL
Denotational semantics for guarded dependent type theory
我们提出了一个新的模型的保护依赖类型论（GDTT），一个类型论与保护递归和多个时钟，其中一个可以编程，共归纳类型的原因。递归定义的共归纳程序和证明的生产力是使用保护递归编码在类型中的，因此可以模块化地检查，不像现代证明助手中实现的语法检查。该模型基于一类时间对象的协变预层，并使用时钟的预层对时钟进行量化建模。为了模拟时钟无关性公理，这对于使用共归纳类型进行编程至关重要，类型必须被解释为与时钟对象正交的预层。在依赖类型的情况下，这转化为提升条件，类似于在类型论的同伦理论模型中发现的提升条件，但在这里具有提升唯一性的额外要求。由于在这个模型中标准的Hofmann-Streicher构造定义的宇宙不满足这个性质，GDTT中的宇宙必须通过时钟变量的上下文来索引。我们展示了如何模拟这些宇宙的方式，时钟上下文的夹杂物引起的夹杂物的宇宙与类型操作的鼻子。
2020-04-13 cs.LO
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
本文在守护类型论中利用高阶归纳类型和守护递归建模带概率选择与递归类型的语言，并建立操作与指称语义间的关系以支持充分性和上下文等价推理。
2024-10-24 cs.LO cs.PL
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
守护递归是一种强大的模式递归方法，可以看作是步进索引的抽象形式。它目前被广泛用于分离逻辑，通过求解具有负出现的域方程来模拟具有高级功能的程序设计语言。在其多时钟版本中，保护递归也可以用于对共归纳类型进行编程和推理，编码类型中递归定义所需的生产力条件。本文提出了第一种类型论，它结合了多时钟保护递归和立方类型论的特点，并给出了一个指称语义。结合使用高阶归纳类型（Higher Inductive Types，HIT）和保护递归，可以对传统上难以在类型论中表示的共归纳类型进行简单的编程和推理，例如标记转移系统的分支分支类型。例如，我们的研究结果意味着这些双相似性意味着路径平等，因此证明可以沿着双相似性证明。我们的技术贡献之一是一个新的原则下的时钟感应。这允许在时钟上的通用量化与HIT交换直到等价的类型，并且对于共归纳类型的编码至关重要。这种交换性的要求已经制定了归纳类型的公理在以前的类型论与多时钟保护递归，但我们目前的配方作为一个归纳原则允许制定一般的计算规则。
2022-06-03 cs.LO
(Co)recursion in Logic Programming: Lazy vs Eager
CoALP（英语：CoAlgebraic Logic Programming）是逻辑编程的一种方言，旨在为逻辑编程中的递归和共递归函数带来更精确的编译时和运行时终止和生产力分析。它的第二个目标是将类似于函数定理证明器的保护惰性（共）递归引入逻辑编程。在本文中，我们解释了CoALP的懒惰特性，并将其与CoLP中的循环分析和急切执行进行了比较。最后，我们概述了未来的发展方向，在逻辑编程的守护（共）递归。
2014-05-20 cs.LO cs.PL
Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
University of Gothenburg（哥德堡大学）
使用Claude在Agda中自动形式化了哥德尔第二不完备定理，基于Guard的证明大纲，并分析了LLM在数学形式化中的优势与局限。
2026-06-02 cs.LO
On the Meaning of Transition System Specifications
转换系统规范为编程和规约语言提供了语义。它们提供了一个封闭术语作为过程图的含义：一个标记转换系统中的状态。与此同时，它们提供了一个n元运算符的含义，或者更一般地说，一个具有n个自由变量的开放项，作为过程图上的n元运算。这样做的经典方法，闭项语义学，将开放项的含义简化为其闭实例的含义。它使运算符的含义依赖于它所使用的上下文。在这里，我提出了一个替代的过程图语义的TSS，不受这个缺点。流程图上的语义等价可以被提升，以使开放项符合封闭项或流程图语义。对于纯TSS，后者更具鉴别力。我认为五个健全的要求配备了递归结构的编程和规约语言的语义：组合性，适用于n元运算符，递归和变量，不变性下$α$ -转换，递归定义原则，说递归调用的意义应该是相应的递归方程的解决方案。我建立了四个这些要求下的TSS的闭项语义的满意度意味着他们的满意度下的过程图语义。
2019-08-23 cs.LO
Recursive Mutexes in Separation Logic
University of Illinois Chicago（伊利诺伊大学芝加哥分校）；Skylabs AI
本文研究了分离逻辑中递归互斥锁的规范方法，提出了一种统一处理多次获取和释放的规范方式，简化了客户端对锁状态的判断。
2026-01-30 cs.LO cs.PL
A Light Modality for Recursion
本文提出一种语法上静默的模态，用于控制无限结构上递归函数式程序的行为，将递归控制负担从程序员转移到编译器，并引入带静默模态和守护递归类型的类型化lambda演算，保证归一化且可推断类型。
2019-02-02 cs.LO cs.PL
Elgot Algebras
指称语义可以基于具有附加结构（序、度量等）的代数。这使得解释递归规范成为可能。Elgot的想法是将指称语义建立在迭代理论的基础上，即，抽象递归规范要求有唯一解的理论。后来布卢姆和Esik研究迭代理论和迭代代数，其中一个指定的解决方案必须遵守某些公理。在本文中，我们提出了所谓的Elgot代数作为一个方便的结构语义。Elgot代数是一个对每个平坦递归方程组都有特定解的代数。该规范满足两个简单且动机良好的公理：函数性（声明在递归变量重命名下解是稳定的）和组合性（声明如何执行同时递归）。这两个公理干规范从Elgot的迭代理论：我们证明了范畴的Elgot代数是Eilenberg-Moore范畴的单子由一个自由的迭代理论。
2006-11-08 cs.LO math.CT
Synthesis from Recursive-Components Libraries
综合是根据系统的规范自动构造系统。在经典的综合算法中，它总是假设系统是“从头开始构建”，而不是由可重用的组件组成。当然，这在现实生活中很少发生。在现实生活中，几乎每一个重要的商业软件系统都严重依赖于使用可重用组件库。此外，其他上下文，如Web服务编排，可以建模为从组件库合成系统。2009年，我们引入了基于可重用组件库的LTL合成。在这里，我们扩展的工作和学习的综合从组件库与“调用和返回”的控制流结构。这种控制流结构在软件系统中非常常见。我们定义的嵌套词时序逻辑（NWTL）的递归组件库，其中NWTL是一个规范的形式主义，比LTL更丰富，这是适合于“调用和返回”的计算合成的问题。我们解决了这个问题，提供了一个综合算法，并显示该问题是2EXPTIME完全的，作为标准的综合。
2011-06-07 cs.LO cs.SE
The very dependent recursive structure of iterated parametricity in indexed form
Université Paris Cité, Inria, CNRS, IRIF（巴黎西岱大学、法国国家信息与自动化研究所、法国国家科学研究中心、IRIF）
本文研究了迭代参数性在索引形式中的依赖结构，通过定义性推理替代等式推理，提出了一种高度依赖的构造方法。
2026-02-13 cs.LO
On Recursive Operations Over Logic LTS
最近，为了在一个统一的框架中混合代数和逻辑风格的规格说明，逻辑标记的转换系统（逻辑LTS或LLTS简称）的概念已经被引入和探索。给出了LLTS上的各种构造子，包括常用的过程代数算子、逻辑连接词（合取和析取）和标准时态算子（always和unless）。然而，迄今为止，还没有人试图发展关于LLTS上的（嵌套）递归运算的一般理论，并且一些基本问题仍然是开放的。本文拟用纯过程代数的方法研究这一问题。一些基本的性质，包括预同余和一致解的唯一性方程，将建立。
2013-11-25 cs.LO cs.SE
Mechanizing Coinduction and Corecursion in Higher-order Logic
递归和上递归定义的理论已经在高阶逻辑（HOL）中得到了发展，并使用Isabelle进行了机械化。最小不动点表示归纳数据类型，如严格列表;最大不动点表示共归纳数据类型，如懒惰列表。良基递归表示归纳数据类型上的递归函数;协递归表示产生共归纳数据类型元素的函数。该理论依赖于传统的形式化的无限树。该理论旨在用于规范和验证。它支持大范围的可计算函数的推理，但没有形式化它们的操作语义，也可以表示不可计算函数。该理论说明使用有限和无限的列表。共递归表示无限列表上的函数;共归纳推理这类函数。
2000-10-31 cs.LO
Verification of Component-based Systems with Recursive Architectures
研究了参数化构件系统的可靠性验证方法。该方法使用了资源逻辑，一种新的正式规约语言的分布式系统组成的一个有限的，但无界数量的组件。该逻辑允许通过与用于描述代数数据类型或递归数据结构的归纳定义类似的归纳定义来描述协调有限数量类型的组件的实例的架构配置。对于这种逻辑中指定的参数系统，我们表明，决策问题，如达到死锁或违反临界区是不可判定的，在一般情况下。尽管这个负面的结果，我们提供了这些决策问题的实际半算法依赖于自动合成的结构不变允许一般的安全性能的证明。使用一元二阶逻辑的WSkS片段定义不变量，已知其可由经典自动机逻辑连接判定，从而将验证问题减少到检查WSkS公式的可满足性。
2021-12-15 cs.FL cs.LO
Semantics of Higher-Order Recursion Schemes
高阶递归格式是递归方程，它从给定的称为“终端”的操作定义新的操作。每个这样的递归方案都被证明在每个斯科特的λ-演算模型中具有最少解释的语义，其中终端被解释为连续操作。对于基于无限λ-项的不可解释语义，我们遵循Fiore，Plotkin和Turi的思想，在上下文中的集合范畴中工作，它是有限集合范畴上的预层。Fiore等人展示了如何通过内函子Hλ来捕获λ-演算中变量绑定的类型，并且他们通过证明λ-项的预层是初始Hλ-幺半群来解释λ-项的同时替换。这里我们研究有理无限λ-项的预层，并证明这是一个初始迭代Hλ-幺半群。我们的结论是，每一个守卫高阶递归计划有一个唯一的未解释的解决方案在这个幺半群。
2011-04-20 cs.LO math.CT
