一句话：提出 DeLaM 分层模态依赖类型理论，支持开放代码的引用、组合、递归分析与类型安全代码生成。
论文提出 DeLaM，一种面向 Martin-Löf 类型论（MLTT）元编程的依赖分层模态类型理论。DeLaM 分为三层：无计算的 MLTT 静态语法对象层、带计算行为的纯 MLTT 层，以及支持引用开放代码、组合和递归分析的元编程层；代码对象也可在元编程层执行。随层级上升，表达力严格增强：代码对象仅描述静态语法，而计算发生在 MLTT 层与元编程层。该工作为同时支持类型安全代码生成与代码分析的元编程提供依赖类型基础，并用 Kripke 逻辑关系证明弱规范化与可转换性判定性。
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.
@article{HuP25,
title = {A Dependent Type Theory for Meta-programming with Intensional Analysis},
author = {Jason Z. S. Hu and Brigitte Pientka},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704851}
}