A Dependent Type Theory for Meta-programming with Intensional Analysis

In this paper, we introduce DeLaM , a dependent layered modal type theory which enables meta-programming in Martin-Löf type theory (MLTT) with recursion principles on open code. DeLaM includes three layers: the layer of static syntax objects of MLTT without any computation, the layer of pure MLTT with the computational behaviors, and the meta-programming layer, which extends MLTT with support for quoting an open MLTT code object, composing, and analyzing open code using recursion. We can also execute a code object at the meta-programming layer. The expressive power strictly increases as we move up in a given layer. In particular, while code objects only describe static syntax, we allow computation at the MLTT and meta-programming layer. As a result, DeLaM provides a dependently typed foundation for meta-programming that supports both type-safe code generation and code analysis. We prove the weak normalization of DeLaM and the decidability of convertibility using Kripke logical relations.