WG211/M25Murase

Kiselyov et al. introduced the notion of refined environment classifiers, which ensure scope-safe code generation with mutable state by annotating code types with *classifiers* that record the scoping information of code fragments. While their proposal was developed for a two-level, combinator-based code-generation language, we adapt their idea to quasi-quotation-based multi-stage programming in the style of MetaML.

The resulting language guarantees scope-safe code generation even in the presence of mutable state, thereby resolving the long-standing issue of scope extrusion in MetaML. We also show that our language can express a form of cross-stage persistence, and that **polymorphism over classifiers** can be incorporated into the type system to further enhance its expressiveness.