一句话：提出守卫计算类型论，将 Nakano later 模态、时钟变量与依赖类型及宇宙层级相结合。
论文研究如何在依赖类型论中容纳 Nakano 的 later 模态与时钟变量，以刻画因果、同步递归函数以及更广的生产性（共）程序。此前这些构造难以与依赖类型结合，同时保持类型论的操作意义并支持宇宙层级 Ui。作者提出守卫计算类型论（Guarded Computational Type Theory），在计算类型论框架中引入守卫构造，使 later 模态、时钟变量与依赖类型、宇宙层级相容。该工作为在保持可执行语义的同时定义因果与生产性程序提供了类型论基础，并解决了与 Ui 层级共存的问题。
Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has been difficult to combine these constructs with dependent types in a way that preserves the operational meaning of type theory and admits a hierarchy of universes Ui.