Closed types for a safe imperative MetaML

Abstract

This paper addresses the issue of safely combining computational effects and multi-stage programming. We propose a type system which exploits a notion of closed type, to check statically that an imperative multi-stage program does not cause run-time errors. Our approach is demonstrated formally for a core language called MiniMLrefmeta. This core language safely combines multi-stage constructs and ML-style references, and is a conservative extension of MiniMLref. a simple imperative subset of SML. In previous work, we introduced a closed type constructor, which was enough to ensure the safe execution of dynamically generated code in the pure fragment of MiniMLrefmeta.