Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation

Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann

Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation

Nick Benton ,
Andrew Kennedy ,
Lennart Beringer ,
Martin Hofmann

Proceedings of the Ninth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP '07) | July 2007

Published by ACM

Download BibTex

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 transformations.