**Relational Semantics for Effect-Based Program Transformations: Higher-Order Store**

Nick Benton, Andrew Kennedy, Martin Hofmann and Lennart Beringer.
In The 11th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'09), September 2009.

We give a denotational semantics to a region-based effect system
tracking reading, writing, and allocation in a higher-order
language with dynamically allocated references *of arbitrary type
including effect-triggering functions*.
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.

**Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation**

Nick Benton, Andrew Kennedy, Martin Hofmann and Lennart Beringer.
In The Ninth ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'07), July 2007.

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-based program equivalences and can thus serve as a foundation for effect-based compiler transformations.

**Reading, Writing and Relations: Towards Extensional Semantics for Effect Analyses**

Nick Benton, Andrew Kennedy, Martin Hofmann and Lennart Beringer.
In The Fourth Asian Symposium on Programming Languages and Systems (APLAS 2006), Sydney, Australia, November 2006.
(Slides from talk: ppt pdf)

We give an elementary semantics to an effect system, tracking read and write effects by using relations over a standard extensional semantics for the original language. The semantics establishes the soundness of both the analysis and its use in effect-based program transformations.

**Monads, Effects and Transformations**

Nick Benton and Andrew Kennedy. In The Third International Workshop on Higher Order
Operational Techniques in Semantics (HOOTS), Paris, France,
September 1999.

Published as Volume 26 in Electronic
Notes in Theoretical Computer Science, Elsevier.

We define a typed compiler intermediate language, MIL-lite, which incorporates computational types refined with effect information. We characterise MIL-lite observational congruence by using Howe's method to prove a ciu theorem for the language in terms of a termination predicate defined directly on the term. We then define a logical predicate which captures an observable version of the intended meaning of each of our effect annotations. Having proved the fundamental theorem for this predicate, we use it with the ciu theorem to validate a number of effect-based transformations performed by the MLj compiler for Standard ML.