@inproceedings{5995c234253347cd9d2c0eca1d10e1b9,

title = "Relational semantics for effect-based program transformations: Higher-order store",

abstract = "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 mixed-variance 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.",

keywords = "Domain theory, Logical relations, Program transformation, Type and effect systems",

author = "Nick Benton and Andrew Kennedy and Lennart Beringer and Martin Hofmann",

year = "2009",

doi = "10.1145/1599410.1599447",

language = "English (US)",

isbn = "9781605585680",

series = "PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming",

pages = "301--311",

booktitle = "PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming",

note = "11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP'09 ; Conference date: 07-09-2009 Through 09-09-2009",

}