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∞, 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∞, 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∞. Fair termination in CSLL∞ follows from cut elimination in μMALL∞.
On the Fair Termination of Client-Server Sessions
Luca Padovani
2022-01-01
Abstract
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∞, 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∞, 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∞. Fair termination in CSLL∞ follows from cut elimination in μMALL∞.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
