论文标题
会话类型的二元性：最终削减
Duality of Session Types: The Final Cut
论文作者
论文摘要
双重性是会话类型理论中的核心概念。 由于在递归类型的二元定义中发现了一个缺陷，因此已经发布了其他几种定义。由于它们的联系并不明显，因此我们比较竞争的定义，讨论权衡并证明了一些等价。某些结果是在AGDA中机械化的。
Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda.
