一句话：提出 Clocked Cubical Type Theory，结合多时钟守卫递归与立方类型论，并用时钟下归纳编码余归纳类型。
本文提出 Clocked Cubical Type Theory，这是首个将多时钟守卫递归（guarded recursion）与立方类型论（Cubical Type Theory）特性结合的类型论。守卫递归是步索引（step-indexing）的抽象形式，多时钟版本可用于余归纳编程与推理，并在类型中编码生产性。作者将其与高阶归纳类型（HITs）结合，使编码可扩展到传统类型论难以表示的余归纳类型，例如有限分支标记迁移系统。技术贡献包括“时钟下的归纳”新原则，为主要编码公理提供计算内容，并在预层模型（presheaf model）中给出指称语义验证。
We present Clocked Cubical Type Theory, the first type theory combining multi-clocked guarded recursion with the features of Cubical Type Theory. Guarded recursion is an abstract form of step-indexing, which can be used for construction of advanced programming language models. In its multi-clocked version, it can also be used for coinductive programming and reasoning, encoding productivity in types. Combining this with Higher Inductive Types (HITs) the encoding extends to coinductive types that are traditionally hard to represent in type theory, such as the type of finitely branching labelled transition systems. Among our technical contributions is a new principle of induction under clocks, providing computational content to one of the main axioms required for encoding coinductive types. This principle is verified using a denotational semantics in a presheaf model.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{KristensenMV22,
title = {Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks},
author = {Magnus Baunsgaard Kristensen and Rasmus Ejlers Mogelberg and Andrea Vezzosi},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533359}
}