论客户端-服务器会话的公平终止

客户端-服务器会话基于一种对传统线性逻辑命题作为会话类型解释的变化，其中非线性通道（那些调节客户端池与单一服务器之间交互的通道）由共指数而非通常的指数来类型化。共指数使得对竞争交互的建模成为可能，即客户端竞争与单一服务器交互，而服务器的内部状态（从而所提供的服务）可随着服务器顺序处理请求而改变。本文给出 CSLL$^\infty$（一个客户端-服务器会话核心演算）的公平终止结果。我们设计了一个类型系统，使得每个良类型项对应于 $\mu$MALL$^\infty$（具有最小和最大不动点的线性逻辑无穷证明论）中的有效推导。然后我们建立演算中的归约与 $\mu$MALL$^\infty$ 中主归约之间的对应关系。CSLL$^\infty$ 中的公平终止由 $\mu$MALL$^\infty$ 中的割消去除得到。