Technical Report No. 172 - Abstract

Simon Helsen
An Equational Theory for a Region Calculus

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 our region calculus. We show that bisimilarity includes the equational theory and that it coincides with contextual equivalence.