作为依赖右伴随的滴答时钟：时钟类型理论的指称语义
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
AI总结：
本文为时钟类型理论（CloTT）构建指称语义，利用依赖右伴随函子建模滴答概念，以支持余归纳推理，并改进了先前有缺陷且复杂的模型。
摘要：
时钟类型理论（CloTT）是一种用于保护递归的类型理论，适用于余归纳类型的编程，允许将生产率编码在类型中，并利用抽象形式的步进索引来推理高级编程语言特性。此前已证明 CloTT 具有多种语法性质，包括强规范化、规范性以及等式理论的可判定性。本文为 CloTT 提出了一种指称语义，有助于研究 CloTT 未来扩展，例如添加路径类型等构造。构建该模型的主要挑战在于对 CloTT 中用于余归纳类型余归纳推理的时钟上的滴答概念进行建模。我们基于一个先前用于建模多时钟保护递归的范畴。在该范畴中存在时钟对象但没有滴答对象，因此上下文中的滴答假设无法使用标准工具进行建模。取而代之，我们使用依赖右伴随函子来建模滴答，这是范畴论中伴随概念到带族范畴（categories with families）的推广。已知依赖右伴随可建模 Fitch 风格模态类型，但在 CloTT 的情形中，模态算子构成一个由类型理论内部时钟索引的族。我们利用时钟对象上的切片范畴中的依赖右伴随来建模该族。最后，我们展示了如何使用语义替换来建模 CloTT 的滴答常量。本工作改进了前两位作者先前提出的模型，该模型不仅存在缺陷，而且相当复杂。
英文摘要：
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of the equational theory. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types. The main challenge for constructing this model is to model the notion of ticks on a clock used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion with multiple clocks. In this category there is an object of clocks but no object of ticks, and so tick-assumptions in a context can not be modelled using standard tools. Instead we model ticks using dependent right adjoint functors, a generalisation of the category theoretic notion of adjunction to the setting of categories with families. Dependent right adjoints are known to model Fitch-style modal types, but in the case of CloTT, the modal operators constitute a family indexed internally in the type theory by clocks. We model this family using a dependent right adjoint on the slice category over the object of clocks. Finally we show how to model the tick constant of CloTT using a semantic substitution. This work improves on a previous model by the first two named authors which not only had a flaw but was also considerably more complicated.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
