Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann (2009)

# Relational semantics for effect-based program transformations: higher-order store

In: PPDP, pp. 301-312.

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. The semantics validates a number of effect-dependent program equivalences and can thus serve as a foundation for effect-based compiler transformations. The definition of the semantics requires the solution of a mixedvariance equation which is not accessible to the hitherto known methods. We illustrate the difficulties with a number of$~$ small example equations one of which is still not known to have a solution.

Document Actions