Higher-Order and Symbolic Computation, 17(4)
Bisimilarity for the Region CalculusSimon Helsen, Department of Electrical and Computer Engineering, University of Waterloo, Canada
|
Abstract: A region calculus is a programming language calculus
with explicit instrumentation for memory management. Every value is
annotated with a region in which it is stored and 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 present a theory based on bisimulation, which serves as a coinductive proof principle for showing equivalences of polymorphically region-annotated terms. Our notion of bisimilarity is reminiscent of open bisimilarity for the pi-calculus and we prove it sound and complete with respect to Morris-style contextual equivalence. As an application, we formulate a syntactic equational theory, which is used elsewhere to prove the soundness of a specializer based on region inference. We use our bisimulation framework to show that the equational theory is sound with respect to contextual equivalence. Keywords: bisimulation, contextual equivalence, equational theory, region calculus |
This article is not yet available online.
![[picture of journal cover]](../LISP.JPG)