一句话：提出 Clocked Type Theory，为守卫递归给出适合归约语义的类型论，并证明合流、强规范化与典范性。
守卫递归（Nakano 意义）允许在类型论中加入一般递归类型与项而不破坏一致性，并已用于余数据编程、余归纳类型推理以及高级语言特性的步进索引。本文旨在为其构造可直接归约、最终可机器检验的实现基础。作者提出 Clocked Type Theory：一种比现有守卫递归类型论更适合归约语义的新类型论，显式引入时钟以控制延迟与守卫。论文证明其归约语义满足合流性、强规范化与典范性，并展示如何编码以流为例的余归纳类型，进而推出该类型系统保证流定义的生产性。
Guarded recursion in the sense of Nakano allows general recursive types and terms to be added to type theory without breaking consistency. Recent work has demonstrated applications of guarded recursion such as programming with codata, reasoning about coinductive types, as well as constructing and reasoning about denotational models of general recursive types. Guarded recursion can also be used as an abstract form of step-indexing for reasoning about programming languages with advanced features. Ultimately, we would like to have an implementation of a type theory with guarded recursion in which all these applications can be carried out and machine-checked. In this paper, we take a step towards this goal by devising a suitable reduction semantics. We present Clocked Type Theory, a new type theory for guarded recursion that is more suitable for reduction semantics than the existing ones. We prove confluence, strong normalisation and canonicity for its reduction semantics, constructing the theoretical basis for a future implementation. We show how coinductive types as exemplified by streams can be encoded, and derive that the type system ensures productivity of stream definitions.