Relational semantics for effect-based program transformations
Nick Benton, Andrew John Kennedy, Lennart Beringer, Martin O. Hofmann · 2009
We give a denotational semantics to a type and effect system tracking reading and writing to global variables holding values that may include higher-order effectful functions. Refined types are modelled as partial equivalence relations over a recursively-defined domain interpreting the untyped language, with effect information interpreted in terms of the preservation of certain sets of binary relations on the store.