JavaScript is disabled for your browser. Some features of this site may not work without it.
Monadic Regions: Formal Type Soundness and Correctness

Author
Fluet, Matthew
Abstract
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.
Date Issued
2004-04-22Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2004-1936
Type
technical report