MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Layered Modal ML (LMML), \textit{the first metaprogramming language that supports storing and running open code under a strong type safety guarantee}. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for LMML, establishing \textit{the first full abstraction result for an imperative MetaML-style language}. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

翻译：MetaML风格的元编程语言允许程序员构造、操作和运行代码。在存在代码的高阶引用时，确保类型安全性具有挑战性，因为自由变量可能逃逸其绑定作用域。本文提出分层模态ML（LMML），\textit{这是首个在强类型安全保证下支持存储和运行开放代码的元编程语言}。其类型系统利用上下文模态类型来显式追踪和推理代码中的自由变量。基于元编程的程序优化中的一个关键问题是优化后的程序是否保持原始程序的语义。回答该问题需要程序等价性的概念以及相应的推理技术。本文提出了一个为LMML捕获上下文等价性的语义模型，从而建立了\textit{面向命令式MetaML风格语言的第一个完全抽象性结果}。我们的模型基于通过操作博弈语义推导的迹，其中程序的意义通过其与环境可能的交互进行建模。我们还建立了一个新颖的闭实例使用定理，该定理同时考虑了按值调用和按名调用的闭包替换。