存在高阶引用时的类型同构（扩展版）
计算机科学中的逻辑
2015-07-01 v2
摘要
我们研究了存在高阶引用时的类型同构问题。首先引入一种带有和类型与高阶引用的有限编程语言，并遵循 Abramsky、Honda 和 McCusker 的工作为其构建了一个完全抽象的博弈模型。通过解决 Laurent 提出的一个开放问题，我们证明了两个有限分支竞技场是同构的，当且仅当它们在动作重命名下几何相同（Laurent 森林同构）。由此我们推导出一个等式理论，用于刻画该语言中的类型同构。然而，我们指出 Laurent 的猜想在无限分支竞技场上不成立，这在带有自然数的语言变体中产生了新的非平凡类型同构。
引用
@article{arxiv.1207.3223,
title = {Isomorphisms of types in the presence of higher-order references (extended version)},
author = {Pierre Clairambault},
journal= {arXiv preprint arXiv:1207.3223},
year = {2015}
}