AI 中文总结
本文针对带可变状态的MetaML风格多阶段编程，提出改进型环境分类器类型系统，排除有害作用域外溢，实现多级代码生成等功能，在Rocq中完成实现与机械化证明。
AI 中文摘要
MetaML风格的多阶段编程（MSP）支持基于准引用的代码生成、生成代码的运行时执行以及跨阶段持久化（CSP），但它与计算效应的交互十分微妙：可变状态会引发作用域外溢，即生成代码会脱离其所依赖变量的作用域。本文提出一种带可变状态的MetaML风格MSP类型系统，可静态排除有害的作用域外溢，同时支持多级代码生成、运行时执行及一种变体CSP。该系统基于改进型环境分类器（RECs），该规范在代码类型中注释生成代码所依赖的变量作用域；为将RECs扩展至MetaML风格场景，我们改进分类器使其不仅跟踪变量作用域，还跟踪分类器自身的作用域，同时集成分类器多态性，支持多级场景中更通用、可复用的代码生成模式。针对所得系统，我们通过定义式解释器定义操作语义，并证明类型健全性及离线代码生成的安全性，表明生成代码可作为独立的良类型程序提取；我们在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.
