多模态依赖类型理论
Multimodal Dependent Type Theory
AI总结：
本文提出多模态依赖类型理论MTT，以模式理论为参数，统一保护递归、公理凝聚等模态情境，并证明其一致性与规范性。
摘要：
我们引入了MTT，一种支持多种模态的依赖类型理论。MTT以模式理论为参数，该模式理论指定了模式、模态及它们之间变换的集合。我们表明，不同的模式理论选择使我们能够使用相同的类型理论在许多模态情境中进行计算和推理，包括保护递归、公理凝聚和参数量化。我们重现了先前在保护递归和公理凝聚方面的工作中的示例，从而证明MTT构成了一种简单且可用的语法，其实例化直观地对应于先前手工构建的模态类型理论。在某些情况下，将MTT实例化到特定情境会揭示出先前未知的类型理论，该理论改进了先前的系统。最后，我们研究了MTT的元理论。我们证明了MTT的一致性，并通过扩展最近的类型理论粘合技术建立了规范性。这些结果不依赖于模式理论的选择，因此适用于广泛的模态情境。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
