A Fully Abstract Trace Semantics for General References
A Fully Abstract Trace Semantics for General References
复制标题
供一般参考的完全抽象跟踪语义
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
J. Laird
中科院分区：
文献类型：
--
作者：
J. Laird
我们描述了一种具有本地声明一般引用的函数式语言（标准 ML 的一个片段）的完全抽象跟踪语义。该语义基于一个双方 LTS，其中状态在程序和环境配置之间交替，标签只携带（一组）基本值、位置和指针名称。程序与环境之间的交互要么是直接的（启动或终止子程序），要么是间接的（通过覆盖共享位置）：操作通过对存储的共享部分进行更新来反映这一点。
We describe a fully abstract trace semantics for a functional language with locally declared general references (a fragment of Standard ML). It is based on a bipartite LTS in which states alternate between program and environment configurations and labels carry only (sets of) basic values, location and pointer names. Interaction between programs and environments is either direct (initiating or terminating subprocedures) or indirect (by the overwriting of shared locations): actions reflect this by carrying updates to the shared part of the store.