Technical Report No. 148 - Abstract

Cristiano Calcagno, Simon Helsen, Peter Thiemann
Syntactic Type Soundness Results for the Region Calculus

The region calculus of Tofte and Talpin is a polymorphically typed lambda calculus with annotations that make memory allocation and deallocation explicit. It is intended as an intermediate language for implementing ML without garbage collection. Static region and effect inference can be used to generate annotations from a given ML program. Soundness of the calculus with respect to the region and effect system is crucial to guarantee safe deallocation of regions, i.e., deallocation should only take place for objects which are provably dead. The original soundness proof by Tofte and Talpin requires a complex co-inductive safety relation. In this paper, we present two small-step operational semantics for the region calculus and prove their soundness. Following the syntactic approach of Wright, Felleisen, and Harper, we obtain simple inductive proofs. The first semantics is store-less. It is simple and elegant and gives rise to perspicuous proofs. The second semantics provides a store-based model for the region calculus. It is slightly more complicated, but includes operations on references with destructive update. We prove (the pure fragment of) both semantics equivalent to the original evaluation-style formulation by Tofte and Talpin.