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

• Type: Conference
• Year: 2007
• Where: PPDP
• Authors: Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
• Keywords: Certain Binary Relations, Denotational Semantics, PPDP 2007, Programming Languages