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}
}