Closed types for a safe imperative {MetaML} : dart-reports : Cal+Mog+She:JFP-ta

C. Calcagno, E. Moggi, and T. Sheard

Closed types for a safe imperative MetaML

J. Funct. Programming, to appear

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 MiniML_ref^meta. This core language safely combines multi-stage constructs and ML-style references, and is a conservative extension of MiniML_ref, 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 MiniML_ref^meta.

[ bib | .pdf ]

Back

This file has been generated by bibtex2html 1.43