@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",
}