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为证明辅助工具提供了支持类型安全策略机制的可靠理论基础。