一句话：提出 MTT：由 mode theory 参数化的多模态依赖类型论，统一涵盖守卫递归、公理凝聚与参数量化等情形。
论文提出 MTT（Multimodal Type Theory），一种支持多种模态的依赖类型论。MTT 由一个 mode theory 参数化，后者规定一组 mode、modality 以及它们之间的变换。通过选择不同的 mode theory，同一套类型论即可用于多种模态场景下的计算与推理，包括守卫递归（guarded recursion）、公理凝聚（axiomatic cohesion）和参数量化（parametric quantification）。作者复现了先前工作在守卫递归与公理凝聚中的例子，说明 MTT 是一种简单可用的语法，其实例化结果直觉上对应以往手工构造的模态类型论；在某些情况下，实例化还产生了优于既有系统的新类型论。在元理论方面，作者证明 MTT 的一致性，并通过扩展近期的类型论 gluing 技术建立 canonicity。这些结果不依赖于 mode theory 的具体选择，因而适用于广泛的模态情形。
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.
@article{paperbot1291,
title = {Multimodal Dependent Type Theory},
author = {Daniel Gratzer and G. A. Kavvos and Andreas Nuyts and Lars Birkedal},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:11)2021}
}