Monads, Effects and Transformations

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.