@inproceedings{321951166ceb43899b8fd7fa2d8885fa,
title = "Relational semantics for effect-based program transformations with dynamic allocation",
abstract = "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.",
keywords = "Logical relations, Parametricity, Program transformation, Region analysis, Type and effect systems",
author = "Nick Benton and Andrew Kennedy and Lennart Beringer and Martin Hofmann",
year = "2007",
doi = "10.1145/1273920.1273932",
language = "English (US)",
isbn = "1595937692",
series = "PPDP'07: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming",
pages = "87--96",
booktitle = "PPDP'07",
note = "9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'07 ; Conference date: 14-07-2007 Through 16-07-2007",
}