Institut für Informatik

Technical Report No. 179 - Abstract

Simon Helsen
An Equational Theory for a Region Calculus - Revised

A region calculus is a polymorphically typed lambda calculus with explicit memory management primitives. Every value is annotated with a region in which it is stored. Regions are allocated and deallocated in a stack-like fashion. The annotations can be statically inferred by a type and effect system, making a region calculus suitable as an intermediate language for a compiler of statically typed programming languages. Although a lot of attention has been paid to type soundness properties of different flavors of region calculi, it seems that little effort has been made to develop a semantic framework. In this paper, we formulate a syntactic equational theory, which is proven sound with respect to contextual equivalence. Soundness is achieved by introducing an appropriate notion of bisimilarity, which provides a co-inductive proof principle for showing equivalences in the region calculus. We show that our notion of bisimilarity includes the equational theory and that it coincides with contextual equivalence.

Report No. 179 (PostScript)