We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Normalization by evaluation for modal dependent type theory.
- Authors
HU, JASON Z. S.; JANG, JUNYOUNG; PIENTKA, BRIGITTE
- 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.
- Subjects
ALGORITHMS
- Publication
Journal of Functional Programming, 2023, Vol 33, p1
- ISSN
0956-7968
- Publication type
Article
- DOI
10.1017/S0956796823000060