一句话：证明了多模态类型论 MTT 的规范化，并将类型检查与转换判定归约为底层模态相等性，从而给出统一算法。
本文研究多模态依赖类型论 MTT 的元理论。MTT 可统一刻画守卫递归、内部参数性等多种模态类型论，但其类型检查与转换判定缺乏通用算法。作者证明 MTT 的规范化，并说明判定 MTT 中的类型检查与转换可归约为判定底层模态情形中模态的相等性，从而为文献中所有 MTT 实例立即导出类型检查算法。证明推广了合成 Tait 可计算性这一抽象胶合方法以处理模态，且该推广基于 MTT 自身，因此同时构成 MTT 的重要案例研究。
We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof uses a generalization of synthetic Tait computability -- an abstract approach to gluing proofs -- to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.