LIPIcs.TYPES.2022.5.pdf
- Filesize: 0.82 MB
- 21 pages
Document
On the Fair Termination of Client-Server Sessions
Author
Luca Padovani 
-
Part of:
Volume:
28th International Conference on Types for Proofs and Programs (TYPES 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-28
File
Document Identifiers
Author Details
Acknowledgements
The author is grateful to the anonymous reviewers of the TYPES'22 post-proceedings for their helpful comments, observations and suggestions of related work.
Cite AsGet BibTex
Luca Padovani. On the Fair Termination of Client-Server Sessions. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.5
https://doi.org/10.4230/LIPIcs.TYPES.2022.5
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^∞.
Subject Classification
ACM Subject Classification
- Theory of computation → Linear logic
- Theory of computation → Process calculi
- Theory of computation → Program analysis
Keywords
- client-server sessions
- linear logic
- fixed points
- fair termination
- cut elimination
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. Appraising fairness in languages for distributed programming. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23, 1987, pages 189-198. ACM Press, 1987. URL: https://doi.org/10.1145/41625.41642.
- David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, 2022, 2022. URL: https://arxiv.org/abs/2005.08257.
- David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
- Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Proc. ACM Program. Lang., 1(ICFP):37:1-37:29, 2017. URL: https://doi.org/10.1145/3110281.
- Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 611-639. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_22.
- Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Math. Struct. Comput. Sci., 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
- Luca Ciccone and Luca Padovani. An infinitary proof theory of linear logic ensuring fair termination in the linear π-calculus. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.36.
- Amina Doumane. On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes). PhD thesis, Paris Diderot University, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01676953.
- Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Math. Struct. Comput. Sci., 28(7):995-1060, 2018. URL: https://doi.org/10.1017/S0960129516000372.
- Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer, 1986. URL: https://doi.org/10.1007/978-1-4612-4886-6.
- Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In Hartmut Ehrig, Robert A. Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Functional and Logic Programming and Specifications (CFLP), volume 250 of Lecture Notes in Computer Science, pages 52-66. Springer, 1987. URL: https://doi.org/10.1007/BFb0014972.
- Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1-66, 1992. URL: https://doi.org/10.1016/0304-3975(92)90386-T.
- Orna Grumberg, Nissim Francez, and Shmuel Katz. Fair termination of communicating processes. In Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, PODC '84, pages 254-265, New York, NY, USA, 1984. Association for Computing Machinery. URL: https://doi.org/10.1145/800222.806752.
- Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
- Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
- Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
- Wen Kokke, J. Garrett Morris, and Philip Wadler. Towards races in linear logic. Log. Methods Comput. Sci., 16(4), 2020. URL: https://lmcs.episciences.org/6979.
- Leslie Lamport. Fairness and hyperfairness. Distributed Comput., 13(4):239-245, 2000. URL: https://doi.org/10.1007/PL00008921.
- Sam Lindley and J. Garrett Morris. Talking bananas: structural recursion for session types. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 434-447. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951921.
- Zesen Qian, G. A. Kavvos, and Lars Birkedal. Client-server sessions in linear logic. Proc. ACM Program. Lang., 5(ICFP):1-31, 2021. URL: https://doi.org/10.1145/3473567.
- Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.