仿射直觉类型与效应系统：合流性与终止性
计算机科学中的逻辑
2009-12-03 v1
摘要
我们提出了一种仿射直觉类型与效应系统，该系统可以被视为 Barber-Plotkin 对偶直觉线性逻辑向具有效应的多线程程序的扩展。在该系统中，动态生成的值（如引用或通道）被抽象到一个有限的区域集合中。我们引入了一种区域使用原则，该原则蕴含了可类型化程序的合流性（从而蕴含确定性）。此外，我们证明了区域分层原则保证了终止性。
引用
@article{arxiv.0912.0419,
title = {An affine-intuitionistic system of types and effects: confluence and termination},
author = {Roberto Amadio and Patrick Baillot and Antoine Madet},
journal= {arXiv preprint arXiv:0912.0419},
year = {2009}
}