Sciweavers

Share
PPDP
2009
Springer

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

9 years 10 months ago
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 ...
Nick Benton, Andrew Kennedy, Lennart Beringer, Mar
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where PPDP
Authors Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
Comments (0)
books