Region inference decorates a program with "region annotations" that makes memory-management actions explicit. The key properties that one wishes to establish about region inference is "memory safety" and "conditional correctness". Memory safety shows that an annotated program does not go wrong due to memory errors. Conditional correctness shows that, assuming that the region annotated program is memory safe, then its observable semantics is the same as that of the original unannotated program.

We give a brief survey of correctness results in the literature. Except for the seminal paper by Tofte and Talpin, previous work has focused on establishing memory safety. The correctness result by Tofte and Talpin also establishes conditional correctness, but in a complex co-inductive fashion. We present a small language with region annotations and show how to prove both memory safety and conditional correctness in a simple syntactic fashion.