一句话：提出并实现带 S4 必然模态的依赖类型论 MLTT🔒，给出基于 NBE 扩展的类型检查算法及其可靠性与完备性证明。
模态在编程与数学中广泛出现，但在核心依赖类型论中形式化模态仍存在显著技术挑战。本文提出 MLTT🔒，它在标准 Martin-Löf 类型论连接词的基础上加入 S4 风格的必然模态，支持模态类型与依赖类型之间的平滑交互，为编程与综合数学中的模态使用提供共同基础。作者设计并证明了 MLTT🔒 类型检查算法的可靠性与完备性，其核心是一种对归一化求值（normalization by evaluation）的新颖扩展。最后，他们在 MLTT🔒 的原型证明助手中实现了该算法，展示了相关技术的易用性。
Modalities are everywhere in programming and mathematics! Despite this, however, there are still significant technical challenges in formulating a core dependent type theory with modalities. We present a dependent type theoryMLTT🔒supporting the connectives of standard Martin-Löf Type Theory as well as anS4-style necessity operator.MLTT🔒supports a smooth interaction between modal and dependent types and provides a common basis for the use of modalities in programming and in synthetic mathematics. We design and prove the soundness and completeness of a type checking algorithm forMLTT🔒, using a novel extension of normalization by evaluation. We have also implemented our algorithm in a prototype proof assistant forMLTT🔒, demonstrating the ease of applying our techniques.
@article{paperbot589,
title = {Implementing a modal dependent type theory},
author = {Daniel Gratzer and Jonathan Sterling and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341711}
}