Layered Modal Type Theories

TL;DR

This work introduces Layered Modal Type Theories that stratify modal code and computation into distinct layers, enabling pattern analysis on open code and solid semantic guarantees. The authors develop a two-layer (layer 0 for code, layer 1 for computation) framework, provide a rigorous presheaf-model NbE semantics, and establish completeness and soundness results via layered gluing models. They extend the theory with contextual types to support open-code pattern matching, and adapt the presheaf NbE construction to this richer setting, maintaining normalization properties. Finally, they add a recursor for natural numbers, showing the framework can accommodate dependent-like constructs while preserving core meta-programming guarantees. The combination of layered semantics, presheaf NbE, and contextual types offers a principled foundation for meta-programming languages with robust normalization and extensibility.

Abstract

We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.

Theorems & Definitions (102)

• lemma 1
• theorem 1
• theorem 2
• lemma 2: Lifting
• lemma 3
• theorem 3
• lemma 4: Presupposition
• theorem 4: Global substitution
• theorem 5: Local substitution
• theorem 6: Simultaneous substitution