一句话：为支持可变状态的 MetaML 式多阶段编程提出 Refined² 环境分类器类型系统，静态排除有害作用域逃逸。
MetaML 风格多阶段编程支持准引用代码生成、运行时执行和跨阶段持久化，但与可变状态等效应交互微妙：生成代码可能发生作用域逃逸，逃出其依赖变量的作用域。本文为带可变状态的 MetaML 式多阶段编程提出类型系统，静态排除有害作用域逃逸，并支持多级代码生成、运行时执行及一种 CSP 变体。系统基于 refined environment classifiers（RECs），以变量作用域标注代码类型；作者进一步精化分类器，使其同时追踪变量作用域与分类器自身作用域，并引入分类器多态以支持更通用的多级生成模式。论文通过定义性解释器定义操作语义，证明类型可靠性与离线代码生成安全性，表明生成代码可抽取为独立良类型程序，并给出实现和 Rocq 机器化证明。
MetaML-style multi-stage programming (MSP) supports quasi-quotation-based code generation, runtime execution of generated code, and cross-stage persistence (CSP). However, its interaction with computational effects is subtle: mutable state can cause scope extrusion, where generated code escapes the scope of variables on which it depends. This paper presents a type system for MetaML-style MSP with mutable state that statically rules out harmful scope extrusion while supporting multi-level code generation, runtime execution, and a variant of CSP. Our system builds on refined environment classifiers (RECs), a discipline that annotates code types with the variable scopes on which generated code depends. To scale RECs to the MetaML-style setting, we refine classifiers so that they track not only variable scopes, but also the scopes of classifiers themselves. Further, we integrated polymorphism over classifiers, enabling more general and reusable code generation patterns in a multi-level setting. For the resulting system, we define an operational semantics via a definitional interpreter and prove type soundness and safety of offline code generation, showing that generated code can be extracted as standalone well-typed programs. We provide working implementations and mechanized proofs in Rocq.