Region Analysis and the Polymorphic Lambda Calculus

We show how to translate the region calculus of Tofte and Talpin, a typed lambda calculus which can statically delimit the lifetimes of objects into an extension of the polymorphic lambda calculus called F sub #. We give a denotational semantics of F sub #, and use it to give a simple and abstract proof of correctness of memory deallocation.