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中判定类型检查和转换可以归结为判定底层模态情境中模态的等价性，从而直接为文献中MTT的所有实例化提供了一个类型检查算法。该证明使用了合成Tait可计算性——一种胶合证明的抽象方法——的推广，以处理模态。这一推广基于MTT本身，因此该证明也构成了对MTT的一个重要案例研究。