一句话：用博弈语义中的 block-innocent 策略刻画块结构，并比较块存储、纯函数式计算与动态内存分配。
论文用博弈语义研究块结构的语义，并引入 block-innocent 策略来刻画 call-by-value 下带块分配存储的计算。作者证明了可靠性、有限可定义性与万有性，从而可比较纯函数式计算、块存储计算与动态内存分配。结果显示：动态变量分配恰在相关项（开或闭）为基本类型时可替换为块分配变量；涉及二阶类型时，块分配存储可替换为纯函数式计算。论文还证明 call-by-value Idealized Algol 的一个有限片段可判定，而允许动态内存分配会导致不可判定，凸显块结构的限制性。
We study the semantic meaning of block structure using game semantics. To that end, we introduce the notion of block-innocent strategies and characterise call-by-value computation with block-allocated storage through soundness, finite definability and universality results. This puts us in a good position to conduct a comparative study of purely functional computation, computation with block storage as well as that with dynamic memory allocation. For example, we can show that dynamic variable allocation can be replaced with block-allocated variables exactly when the term involved (open or closed) is of base type and that block-allocated storage can be replaced with purely functional computation when types of order two are involved. To illustrate the restrictive nature of block structure further, we prove a decidability result for a finitary fragment of call-by-value Idealized Algol for which it is known that allowing for dynamic memory allocation leads to undecidability.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MurawskiT10,
title = {Block structure vs scope extrusion: between innocence and omniscience},
author = {Andrzej S. Murawski and Nikos Tzevelekos},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 3},
year = {2017},
doi = {10.2168/lmcs-12(3:3)2016}
}