DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
Jason Z. S. Hu, Brigitte Pientka
TL;DR
DeLaM unifies dependent types with a $2$-layered modal type theory to enable type-safe meta-programming and introspective analysis of code. It extends prior layered modal frameworks with context variables, provides a comprehensive syntactic and semantic apparatus (weakening, substitutions, reducibility, and validity judgments), and develops a complete convertibility framework with normalization. The work presents a full dependent extension, including code promotion, non-cumulativity, universe polymorphism, and Tarski-style universes, along with modal and meta-programming constructs for tactics and introspection. Together, these results establish a solid, consistency-preserving foundation for proof assistants that can support type-safe meta-programming and tactic languages within a single, unified theory.
Abstract
We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in which we can not only compose and execute code, but also intensionally analyze the code of types and terms. The latter in particular allows us to write tactics as meta-programs and use regular libraries when writing tactics. DeLaM provides a sound foundation for proof assistants to support type-safe tactic mechanism.