Contextual MetaML: Syntax and Full Abstraction

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 Contextual MetaML, $\mathit{\text{the}}\mathit{\text{first}}\mathit{\text{metaprogramming}}\mathit{\text{language}}\mathit{\text{that}}\mathit{\text{supports}}\mathit{\text{storing}}\mathit{\text{and}}\mathit{\text{running}}\mathit{\text{open}}\mathit{\text{code}}\mathit{\text{under}}\mathit{\text{a}}\mathit{\text{strong}}\mathit{\text{type}}\mathit{\text{safety}}\mathit{\text{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 Contextual MetaML, establishing $\mathit{\text{the}}\mathit{\text{first}}\mathit{\text{full}}\mathit{\text{abstraction}}\mathit{\text{result}}\mathit{\text{for}}\mathit{\text{an}}\mathit{\text{imperative}}\mathit{\text{MetaML-style}}\mathit{\text{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.