Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation

posted by  kevyn (54)  12 months ago (research.microsoft.com)

We give a denotational semantics to a region-based effect system tracking reading, writing and allocation in a higher-order language with dynamically allocated integer references. Effects are interpreted in terms of the preservation of certain binary relations on the store, parameterized by region-indexed partial bijections on locations. The semantics validates a number of effect-dependent program equivalences and can thus serve as a foundation for effect-based compiler