阿贝尔逻辑中的会话类型
计算机科学中的逻辑
2013-12-11 v1 编程语言
摘要
曾有一位博士生说：“我发现了一双木鞋。我在左鞋里放了一枚硬币，在右鞋里放了一把钥匙。第二天早上，我发现这些物体出现在了相反的鞋子里。”我们不声称此类鞋子存在，而是在类型化 lambda 演算的背景下提出了一种类似的编程抽象。其结果被称为 Amida 演算，它扩展了 Abramsky 的线性 lambda 演算 LF 并刻画了阿贝尔逻辑。
引用
@article{arxiv.1312.2700,
title = {Session Types in Abelian Logic},
author = {Yoichi Hirai},
journal= {arXiv preprint arXiv:1312.2700},
year = {2013}
}
备注
In Proceedings PLACES 2013, arXiv:1312.2218