Syntactic Type Soundness for the Region Calculus

11 years 6 months ago
Syntactic Type Soundness for the Region Calculus
The region calculus of Tofte and Talpin is an annotated polymorphically typed lambda calculus which makes memory allocation and deallocation explicit. It is intended as an intermediate language in a compiler for ML-like languages. The region annotations are obtained by static region and effect inference, which makes it an attractive alternative for garbage collection. Soundness of the region and effect system is crucial to guarantee safe deallocation of regions, i.e. deallocation should only take place for objects which are provable dead. Tofte and Talpin have proved type soundness of the region calculus using rulebased co-induction. This proof is quite complicated and not very intuitive. Much of the problem lies in the low-level big-step operational semantics which involves manipulations of an explicit store and which has a co-inductive definition. In this paper, we present a small-step operational semantics for the region calculus, based on syntactic rewriting. We prove type soundne...
Simon Helsen, Peter Thiemann
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2000
Authors Simon Helsen, Peter Thiemann
Comments (0)