一句话：提出模态依赖类型论 Mint，并给出其模块化、可机化的求值规范化证明与算法。
本文提出 Kripke 风格的模态依赖类型论 Mint，将依赖类型与必然模态结合，把 Pfenning–Davies 的模态 λ-演算扩展到完整的 Martin-Löf 类型论，从而涵盖系统 K、T、K4 与 S4 的依赖类型变体，并支持宇宙层级、归纳类型与大消除。论文给出基于无类型域模型的模块化可靠且完备的求值规范化（NbE）证明；该证明无需修改即可适用于上述四种模态系统，并导出可直接实现的规范化算法。作者还在 Agda 中完整机化模型与 NbE 证明，并抽取 Haskell 实现，以强化结果的可信度。
Abstract We present the Kripke-style modal type theory, Mint , which combines dependent types and the necessity modality. It extends the Kripke-style modal lambda-calculus by Pfenning and Davies to the full Martin-Löf type theory. As such it encompasses dependently typed variants of system K , T , K 4, and S 4. Further, Mint seamlessly supports a full universe hierarchy, usual inductive types, and large eliminations. In this paper, we give a modular sound and complete normalization-by-evaluation (NbE) proof for Mint based on an untyped domain model, which applies to all four aforementioned modal systems without modification. This NbE proof yields a normalization algorithm for Mint, which can be directly implemented. To further strengthen our results, our models and the NbE proof are fully mechanized in Agda and we extract a Haskell implementation of our NbE algorithm from it.
@article{paperbot2145,
title = {Normalization by evaluation for modal dependent type theory},
author = {JASON Z. S. HU and JUNYOUNG JANG and BRIGITTE PIENTKA},
journal = {Journal of Functional Programming},
volume = {33},
year = {2023},
doi = {10.1017/s0956796823000060}
}