高阶引用下的类型同构
计算机科学中的逻辑
2011-12-15 v1 计算机科学与博弈论
摘要
我们研究了具有高阶引用的编程语言中的类型同构问题。我们首先回顾了 Abramsky、Honda 和 McCusker 关于高阶引用的博弈论模型。通过解决 Laurent 的一个开放问题，我们证明了两个有限分支竞技场是同构的，当且仅当它们在移动重命名下几何相同（Laurent 的森林同构）。由此我们推导出了一个等式理论，刻画了具有高阶引用的有限语言中的类型同构。然而，我们表明 Laurent 的猜想在无限分支竞技场上不成立，从而在该语言扩展自然数后产生了一个非平凡的类型同构。
引用
@article{arxiv.1112.3198,
title = {Isomorphisms of types in the presence of higher-order references},
author = {Pierre Clairambault},
journal= {arXiv preprint arXiv:1112.3198},
year = {2011}
}
备注
Twenty-Sixth Annual IEEE Symposium on Logic In Computer Science (LICS 2011), Toronto : Canada (2011)