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

Relational semantics for effect-based program transformations: higher-order store
复制标题

基于效果的程序转换的关系语义：高阶存储

DOI：
--
复制
发表时间：
2009
期刊：
ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming
影响因子：
--
通讯作者：
M. Hofmann
M. Hofmann
中科院分区：
--
文献类型：
--
作者：
Nick Benton;A. Kennedy;Lennart Beringer;M. Hofmann

文献摘要

被引文献

相似文献

我们给出了一个类型和效果系统的指称语义，该系统跟踪读取和写入保存值的全局变量，这些变量可能包含高阶有效函数。精细化的类型被建模为解释无类型语言的递归定义域上的部分等价关系，并根据存储中某些二进制关系集的保存来解释效果信息。
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.