A simple region inference algorithm for a first-order functional language (extended version

Abstract. Safe is a first-order eager language with facilities for pro-grammer controlled destruction and copying of data structures. It pro-vides also regions, i.e. disjoint parts of the heap, where the program allo-cates data structures. The runtime system does not need a garbage collec-tor and all allocation/deallocation actions are done in constant time. The language is aimed at inferring and certifying upper bounds for memory consumption in a Proof Carrying Code environment. Some of its analyses have been presented elsewhere [7, 8]. In this paper we present an inference algorithm for annotating programs with regions which is both simpler to understand and more efficient than other related algorithms. Program-mers are assumed to write programs and to declare datatypes without any reference to regions. The algorithm decides the regions needed by every function. It also allows polymorphic recursion with respect to re-gions. We show convincing examples of programs before and after region annotation, prove the correctness and optimality of the algorithm, and give its asymptotic cost.