Monadic Regions: Formal Type Soundness and Correctness

Drawing together two lines of research (that done in type-safe region-based memory management and that done in monadic encapsuation of effects), we give a type-preserving translation from a variation of the region calculus of Tofte and Talpin into an extension of System F augmented with monadic types and operations. Our source language is a novel region calculus, dubbed the Single Effect Calculus, in which sets of effects are specified by a single region representing an upper bound on the set. Our target language is F^RGN, which provides an encapsulation operator whose parametric type ensures that regions (and values allocated therein) are neither accessible nor visible outside the appropriate scope