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

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. Categories and Subject Descriptors F.3.2 [Logic and Meanings of Programs]: Semantics of Programming Languages – Denotational semantics, Program analysis; F.3.2 ...

• Type: Conference
• Year: 2009
• Where: PPDP
• Authors: Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
• Keywords: Denotational Semantics, Partial Equivalence Relations, PPDP 2009, Programming Languages, Variables Holding Values