Region-based memory management was introduced by Tofte and Talpin in the mid-1990's as a compile-time alternative to garbage collection for ML. A special analysis in the compiler, region inference, automatically inserts explicit memory-management operations into the program and also produces a certificate that the annotated program is memory safe, in the form of a typing derivation in a specialized type system. Since then, the idea has been applied to other languages - but only just the part of it that is about mechanically checking that explicit region annotations for a program are safe. Indeed, no account of region inference that is applicable to other languages than ML has been published so far.

This talk describes my ongoing work on formalizing a framework for region-based memory management that allows region inference and checking algorithms to be formulated in way that apply to a wide range of languages. The basic idea is to translate source programs into an abstract flowchart-based intermediate language and develop region inference for the intermediate language. The results of the inference can be translated back to the original program and then compiled to machine (or byte) code using an only lightly modified existing compiler. This design makes it possible to transfer region-inference techniques between host languages with a minimum of re-invention of theory for the recipient language.