多峰类型论的规范化
Normalization for multimodal type theory
摘要：
通过刻画类型论的范式并证明其规范化，我们考虑了多峰类型论（MTT）的转换问题。标准化遵循一个新的适应斯特林的合成泰特可计算性，概括的框架，以适应一个类型论与模态和多种模式。作为我们主要结果的推论，我们将MTT的转换问题归结为其模式论的转换问题，并证明了类型构造子的内射性。最后，我们得出结论，MTT享有可判定的类型检查时，与可判定模式理论实例化。
英文摘要：
We consider the conversion problem for multimodal type theory (MTT) by characterizing the normal forms of the type theory and proving normalization. Normalization follows from a novel adaptation of Sterling's Synthetic Tait Computability which generalizes the framework to accommodate a type theory with modalities and multiple modes. As a corollary of our main result, we reduce the conversion problem of MTT to the conversion problem of its mode theory and show the injectivity of type constructors. Finally, we conclude that MTT enjoys decidable type-checking when instantiated with a decidable mode theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
