Taming Scope Extrusion in Gradual Imperative Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, Rocky Liu

TL;DR
This paper introduces a new gradual metaprogramming language supporting mutable references with guaranteed scope safety through static and dynamic enforcement, addressing scope extrusion issues in imperative metaprogramming.
Contribution
It presents $ ext{lambda}^{, ext{star}}_{ ext{Ref}}$, the first language combining gradual typing, metaprogramming, and mutable references with scope safety, along with its theoretical foundation and implementation.
Findings
Proves type safety and scope safety of the language.
Develops a novel cast calculus for dynamic scope enforcement.
Provides a space-efficient runtime implementation.
Abstract
Metaprogramming enables the generation of performant code, while gradual typing facilitates the smooth migration from untyped scripts to robust statically typed programs. However, combining these features with imperative state - specifically mutable references - reintroduces the classic peril of scope extrusion, where code fragments containing free variables escape their defining lexical context. While static type systems utilizing environment classifiers have successfully tamed this interaction, enforcing these invariants in a gradual language remains an open challenge. This paper presents , the first gradual metaprogramming language that supports mutable references while guaranteeing scope safety. To put on a firm foundation, we also develop its statically typed sister language,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Software Testing and Debugging Techniques
