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.

翻译：我们将分层模态类型理论扩展到依赖类型，提出DeLaM——依赖分层模态类型理论。该类型理论的创新之处在于，我们构建了一个统一类型理论，在其中不仅可以组合和执行代码，还能内涵式分析类型和项的代码。后者特别允许我们编写作为元程序的策略，并在编写策略时使用常规库。DeLaM为证明助手支持类型安全策略机制提供了坚实理论基础。