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^∞.
@InProceedings{padovani:LIPIcs.TYPES.2022.5, author = {Padovani, Luca}, title = {{On the Fair Termination of Client-Server Sessions}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {5:1--5:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.5}, URN = {urn:nbn:de:0030-drops-184485}, doi = {10.4230/LIPIcs.TYPES.2022.5}, annote = {Keywords: client-server sessions, linear logic, fixed points, fair termination, cut elimination} }
Feedback for Dagstuhl Publishing