Summary: Safely adding computational effects to a multi-stage language has been an open problem. In previous work, a closed type constructor was used to provide a safe mechanism for executing dynamically generated code. This paper proposes a general notion of closed type as a simple approach to safely introducing computational effects into multistage languages. We demonstrate this approach formally in a core language called \(\text{Mini-ML}_{\text{ref}}^{\text{BN}}\). This core language combines safely multi-stage constructs and ML-style references. In addition to incorporating state, \(\text{Mini-ML}_{\text{ref}}^{\text{BN}}\) also embodies a number of technical improvements over previously proposed core languages for multi-stage programming.
For the entire collection see [Zbl 0941.00034].