合成保护域理论的第一步：树拓扑中的步索引
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
摘要：
我们提出的拓扑S的树作为一个模型的保护递归。我们研究了内部依赖类型的高阶逻辑的S，并表明S模型的两个模态算子，谓词和类型，作为后卫的递归定义的条款，谓词和类型。特别是，我们将展示如何解决递归类型方程涉及依赖类型。我们建议S的内部逻辑为程序设计语言和程序逻辑的步骤索引模型的抽象版本的合成构造提供了正确的设置。作为一个例子，我们展示了如何构建一个程序设计语言的模型，该语言具有完全在S内部逻辑中的高阶存储和递归类型。此外，我们给出了合成守护整环理论模型的公理化范畴处理，证明了对任何具有良基的完备Heyting代数A，A上层的拓扑构成合成守护整环理论的模型，推广了S的结果.
英文摘要：
We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S. Moreover, we give an axiomatic categorical treatment of models of synthetic guarded domain theory and prove that, for any complete Heyting algebra A with a well-founded basis, the topos of sheaves over A forms a model of synthetic guarded domain theory, generalizing the results for S.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
