一句话：提出用两级类型论（2LTT）实现支持依赖类型与类型级无限制分阶段编译，并给出正确性证明。
分阶段编译旨在支持元编程，同时保证生成代码的良构性，并能简洁混合对象层与元层代码。本文观察到原本为综合同伦论设计的两级类型论（2LTT）也可作为依赖类型分阶段编译的系统。2LTT 规范简洁、模型论性质良好，且支持对象层与元层的丰富语言特性。作者首先概述 2LTT 在 staging 中的特性与应用，然后提出一种“按求值分阶段”（staging-by-evaluation）算法，类比 normalization-by-evaluation，并通过在语义域中求值 2LTT 语法完成分阶段；随后证明算法正确性。该正确性同时构成 2LTT 相对于对象理论的强保守性证明。据作者所知，这是首个支持完整依赖类型和类型无限制分阶段的分阶段编译方案。
The aim of staged compilation is to enable metaprogramming in a way such that we have guarantees about the well-formedness of code output, and we can also mix together object-level and meta-level code in a concise and convenient manner. In this work, we observe that two-level type theory (2LTT), a system originally devised for the purpose of developing synthetic homotopy theory, also serves as a system for staged compilation with dependent types. 2LTT has numerous good properties for this use case: it has a concise specification, well-behaved model theory, and it supports a wide range of language features both at the object and the meta level. First, we give an overview of 2LTT's features and applications in staging. Then, we present a staging algorithm and prove its correctness. Our algorithm is "staging-by-evaluation", analogously to the technique of normalization-by-evaluation, in that staging is given by the evaluation of 2LTT syntax in a semantic domain. The staging algorithm together with its correctness constitutes a proof of strong conservativity of 2LLT over the object theory. To our knowledge, this is the first description of staged compilation which supports full dependent types and unrestricted staging for types.