Title:	Monadic Regions: Formal Type Soundness and Correctness
Authors:	Fluet, Matthew
Keywords:	computer science technical report
Issue Date:	22-Apr-2004
Publisher:	Cornell University
Citation:	http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2004-1936
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.
URI:	http://hdl.handle.net/1813/5647
Appears in Collections:	Computing and Information Science Technical Reports

Files in This Item: File Description Size Format TR2004-1936.pdf 979.85 kB Adobe PDF View/Open

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.