Sciweavers

Share
PPDP
2007
Springer

Relational semantics for effect-based program transformations with dynamic allocation

9 years 10 months ago
Relational semantics for effect-based program transformations with dynamic allocation
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. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features – Dynamic storage management; F.3.2 [Logic and Meanings of Programs]: Semantics of Programming Languages – Denotational semantics, Program analysis; F.3.2 [Logic and Meanings of Programs]: Studies of Program Constructs – Type structure General Terms Languages, Theory Keywords Type and effect systems, region analysis, logical relations, parametricity, program transformation
Nick Benton, Andrew Kennedy, Lennart Beringer, Mar
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where PPDP
Authors Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
Comments (0)
books