Linear Regions Are All You Need
(with Greg Morrisett and Amal Ahmed; Appeared at ESOP'06;
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.
- 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.