Monadic Regions: Formal Type Soundness and Correctness
dc.contributor.author | Fluet, Matthew | en_US |
dc.date.accessioned | 2007-04-04T19:34:51Z | |
dc.date.available | 2007-04-04T19:34:51Z | |
dc.date.issued | 2004-04-22 | en_US |
dc.description.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. | en_US |
dc.format.extent | 1003367 bytes | |
dc.format.mimetype | application/pdf | |
dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2004-1936 | en_US |
dc.identifier.uri | https://hdl.handle.net/1813/5647 | |
dc.language.iso | en_US | en_US |
dc.publisher | Cornell University | en_US |
dc.subject | computer science | en_US |
dc.subject | technical report | en_US |
dc.title | Monadic Regions: Formal Type Soundness and Correctness | en_US |
dc.type | technical report | en_US |
Files
Original bundle
1 - 1 of 1