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.

翻译：我们证明了MTT（一种通用的多模态依赖类型理论）的规范化性质。该理论能够刻画保护递归、内化参数性以及其他多种典型模态情形下的模态类型理论。我们证明，MTT中的类型检查与转换判定可归约为基础模态情境中模态符等式的判定，从而直接为文献中所有MTT实例化方案提供类型检查算法。该证明采用合成Tait可计算性（一种胶结证明的抽象方法）的推广形式来处理模态符。这一扩展本身基于MTT，使得该证明亦成为MTT的重要案例研究。