论多态会话与函数：两个（完全抽象）编码的故事
计算机科学中的逻辑
2018-01-26 v2 编程语言
摘要
本文利用会话类型的逻辑基础来确定 pi-演算的何种类型规则能够精确刻画并被 lambda-演算行为所刻画。借助线性逻辑的相继式演算与自然演绎表述之可靠性与完备性的证明论内容，我们开发了多态会话 pi-演算与 System F 的线性表述之间首对互逆且完全抽象的过程即函数与函数即过程编码。由此我们能够从 lambda-演算理论导出会话演算的结果：(1) 通过其在 System F 中的代数表示刻画归纳与余归纳会话类型；(2) 我们将结果扩展至值与过程传递，从而蕴含强规范化。
引用
@article{arxiv.1711.00878,
title = {On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings},
author = {Bernardo Toninho and Nobuko Yoshida},
journal= {arXiv preprint arXiv:1711.00878},
year = {2018}
}
备注
Extended version of ESOP'18 paper (includes appendix with proofs and additional definitions)