Linear Regions Are All You Need

Abstract. 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, substructural type system. To prove the power of the language, we sketch how Tofte-Talpin-style regions, as well as the firstclass dynamic regions and unique pointers of the Cyclone programming language can be encoded in rgnUL .

• Type: Conference
• Year: 2006
• Where: ESOP
• Authors: Matthew Fluet, Greg Morrisett, Amal J. Ahmed
• Keywords: ESOP 2006, Firstclass Dynamic Regions, LIFO Restriction, Programming Languages, Tofte-Talpin Region Calculus