Linear Regions Are All You Need

esop06.pdf (with Greg Morrisett and Amal Ahmed; Appeared at ESOP'06; 20060327-ESOP06.ppt)
The type-and-effects system of the Tofte-Talpin region calculus makes it possible to safely reclaim objects without a garbage collector. However, it requires that regions have last-in-first-out (LIFO) lifetimes following the block structure of the language. We introduce rgnUL, a core calculus that is powerful enough to encode Tofte-Talpin-like languages, and that eliminates the LIFO restriction. The target language has an extremely simple, sub-structural type system. To prove the power of the language, we sketch how Tofte-Talpin-style regions, as well as the first-class dynamic regions and unique pointers of the Cyclone programming language can be encoded in rgnUL.
Supporting materials:
- rgnURAL.pdf: Complete specification of rgnURAL, including syntax, dynamic semantics (small-step, allocation semantics), and static semantics.
- rgnURAL.tgz: Mechanized proof of type safety in Twelf.

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.