论文标题
关于客户服务器会话的公平终止
On the Fair Termination of Client-Server Sessions
论文作者
论文摘要
客户端服务器会话是基于对线性逻辑命题的传统解释的变化，即会话类型，其中非线性通道（调节客户端与单个服务器之间的相互作用的渠道）由coppertentials键入，而不是通常的指数。共指数实现了赛车交互的建模，使客户竞争与单个服务器进行互动，该服务器的内部状态（以及所提供的服务）可能会随着服务器处理顺序进行处理而发生变化。在这项工作中，我们为CSLL $^\ infty $（客户端服务器会话的核心计算）提供了公平终止结果。我们设计一种类型系统，以使每个良好的术语对应于$μ$ MALL $^\ infty $中的有效派生，这是最少和最大固定点的线性逻辑的无限证明理论。然后，我们建立了微积分的减少与$μ$ MALL $^\ infty $中的原理减少之间的对应关系。 CSLL $^\ infty $中的公平终止是从$μ$ MALL $^\ infty $中的剪切消除中进行的。
Client-server sessions are based on a variation of the traditional interpretation of linear logic propositions as session types in which non-linear channels (those regulating the interaction between a pool of clients and a single server) are typed by coexponentials instead of the usual exponentials. Coexponentials enable the modeling of racing interactions, whereby clients compete to interact with a single server whose internal state (and thus the offered service) may change as the server processes requests sequentially. In this work we present a fair termination result for CSLL$^\infty$, a core calculus of client-server sessions. We design a type system such that every well-typed term corresponds to a valid derivation in $μ$MALL$^\infty$, the infinitary proof theory of linear logic with least and greatest fixed points. We then establish a correspondence between reductions in the calculus and principal reductions in $μ$MALL$^\infty$. Fair termination in CSLL$^\infty$ follows from cut elimination in $μ$MALL$^\infty$.
