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