Region analysis provides a conservative approximation of the lifetimes of objects in higher-order programs. Stemming from earlier work on type and effect calculi, the region system proposed by Tofte and Talpin has led to an implementation of Standard ML based entirely on static memory management.

Extensive research has focused on the optimization and extension of region sys­tems, as well as the subtle problem of formalizing their correctness. Although the classical region calculus of Tofte and Talpin scales suitably to most of the constructs of modem functional languages, relatively little is known about its relation to control mechanisms such as exception handling and the manipulation of reified continuations.

We present a simple and scalable operational framework for proving the correct­ness of region systems based on a variant of the Tofte-Talpin calculus. We then define two extensions to this framework which serve to both clarify and formalize the inter­action between region systems and constructs for generative exceptions and first-class continuations.