The region analysis of Tofte and Talpin is an attempt to
determine statically the life span of dynamically allocated
objects. But the calculus is at once intuitively simple, yet
deceptively subtle, and previous theoretical analyses have
been frustratingly complex: no analysis has revealed and
explained in simple terms the connection between the subtleties
of the calculus and the imperative features it builds on.
We present a novel approach for proving safety and
correctness of a simplified version of the region calculus.
We give a stratified operational semantics, composed of a
high-level semantics dealing with the conceptual difficulties
of effect annotations, and a low-level one with explicit operations
on a region-indexed store. The main results of the paper are
a proof simpler than previous ones, and a modular approach
to type safety and correctness. The flexibility of this approach is
demonstrated by the simplicity of the extension to the full calculus
with type and region polymorphism.