仿射-直觉类型与效应系统：合流性与终止性
计算机科学中的逻辑
2010-05-20 v1
摘要
我们提出了一种仿射-直觉类型与效应系统，可视为 Barber-Plotkin 对偶直觉线性逻辑向带效应的多线程程序的扩展。在该系统中，动态生成的值（如引用或通道）被抽象为有限个区域。我们引入了一种区域使用规范，它保证了可类型化程序的合流性（从而保证了确定性）。此外，我们证明了区域分层规范可确保终止性。
引用
@article{arxiv.1005.0835,
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:1005.0835},
year = {2010}
}