镜像中的会话类型

我们将会话类型重新定义为进程行为相对于其使用的通信通道的投影。在此设定下，我们赋予会话类型一种基于公平测试的语义。由此产生的结果是一个统一的行为类型理论，该理论与对话类型具有共同特征，并涵盖了二元与多方会话类型两者的特性。我们提供的视角阐明了会话类型的本质，并使我们有机会在这样一个框架中对会话类型进行推理：在该框架中，每个概念，从良类型性到会话类型之间的子类型关系，都是基于语义而非语法奠基的。