Document Open Access Logo

An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus

Authors Luca Ciccone , Luca Padovani

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.36.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Author Details

Luca Ciccone
  • University of Torino, Italy
Luca Padovani
  • University of Torino, Italy

Acknowledgements

We are grateful to Simona Ronchi Della Rocca and Francesco Dagnino for their comments on an early draft of this paper, to Stephanie Balzer for having provided pointers to related work and to the anonymous CONCUR reviewers for their questions and detailed feedback.

Cite As Get BibTex

Luca Ciccone and Luca Padovani. An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.36

Abstract

Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of μMALL^∞, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of πLIN, a variant of the linear π-calculus with (co)recursive types into which binary and (some) multiparty sessions can be encoded. As a result we obtain a behavioral type system for πLIN (and indirectly for session calculi through their encoding into πLIN) that ensures fair termination: although well-typed processes may engage in arbitrarily long interactions, they are fairly guaranteed to eventually perform all pending actions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Process calculi
  • Theory of computation → Program analysis
Keywords
  • Linear π-calculus
  • Linear Logic
  • Fixed Points
  • Fair Termination

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Samson Abramsky. Proofs as processes. Theor. Comput. Sci., 135(1):5-9, 1994. URL: https://doi.org/10.1016/0304-3975(94)00103-0.
  2. 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: http://arxiv.org/abs/2005.08257.
  3. 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.
  4. Gianluigi Bellin and Philip J. Scott. On the pi-calculus and linear logic. Theor. Comput. Sci., 135(1):11-65, 1994. URL: https://doi.org/10.1016/0304-3975(94)00104-9.
  5. Luís Caires and Jorge A. Pérez. Multiparty session types within a canonical binary theory, and beyond. In Elvira Albert and Ivan Lanese, editors, Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, volume 9688 of Lecture Notes in Computer Science, pages 74-95. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_6.
  6. 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.
  7. Luca Ciccone, Francesco Dagnino, and Luca Padovani. Fair termination of multiparty sessions. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany, volume 222 of LIPIcs, pages 26:1-26:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.26.
  8. Luca Ciccone and Luca Padovani. A dependently typed linear π-calculus in agda. In PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020, pages 8:1-8:14. ACM, 2020. URL: https://doi.org/10.1145/3414080.3414109.
  9. Luca Ciccone and Luca Padovani. Fair termination of binary sessions. Proc. ACM Program. Lang., 6(POPL):1-30, 2022. URL: https://doi.org/10.1145/3498666.
  10. Luca Ciccone and Luca Padovani. An infinitary proof theory of linear logic ensuring fair termination in the linear π-calculus. Technical report, Università di Torino, 2022. URL: http://www.di.unito.it/~padovani/.
  11. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Inf. Comput., 256:253-286, 2017. URL: https://doi.org/10.1016/j.ic.2017.06.002.
  12. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  13. Farzaneh Derakhshan. Session-Typed Recursive Processes and Circular Proofs. PhD thesis, Carnegie Mellon University, 2021. URL: https://www.andrew.cmu.edu/user/fderakhs/publications/Dissertation_Farzaneh.pdf.
  14. Farzaneh Derakhshan and Frank Pfenning. Circular proofs as session-typed processes: A local validity condition. CoRR, abs/1908.01909, 2019. URL: http://arxiv.org/abs/1908.01909.
  15. Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut reduction in linear logic as asynchronous session-typed communication. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 228-242. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.228.
  16. 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.
  17. Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer, 1986. URL: https://doi.org/10.1007/978-1-4612-4886-6.
  18. Philippa Gardner, Cosimo Laneve, and Lucian Wischik. Linear forwarders. Inf. Comput., 205(10):1526-1550, 2007. URL: https://doi.org/10.1016/j.ic.2007.01.006.
  19. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  20. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  21. 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.
  22. 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.
  23. 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.
  24. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  25. 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.
  26. Naoki Kobayashi. A type system for lock-free processes. Inf. Comput., 177(2):122-159, 2002. URL: https://doi.org/10.1006/inco.2002.3171.
  27. Naoki Kobayashi. Type systems for concurrent programs. In 10th Anniversary Colloquium of UNU/IIST, LNCS 2757, pages 439-453. Springer, 2002. Extended version at http://www.kb.ecei.tohoku.ac.jp/~koba/papers/tutorial-type-extended.pdf. URL: https://doi.org/10.1007/978-3-540-40007-3_26.
  28. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst., 21(5):914-947, 1999. URL: https://doi.org/10.1145/330249.330251.
  29. M.Z. Kwiatkowska. Survey of fairness notions. Information and Software Technology, 31(7):371-386, 1989. URL: https://doi.org/10.1016/0950-5849(89)90159-6.
  30. 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.
  31. Luca Padovani. Fair subtyping for open session types. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 373-384. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_34.
  32. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 72:1-72:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603116.
  33. Luca Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424-464, 2016. URL: https://doi.org/10.1017/S096012951400022X.
  34. Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. URL: https://doi.org/10.1017/S0956796816000289.
  35. 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.
  36. Jean-Pierre Queille and Joseph Sifakis. Fairness and related properties in transition systems - A temporal logic to deal with fairness. Acta Informatica, 19:195-220, 1983. URL: https://doi.org/10.1007/BF00265555.
  37. Pedro Rocha and Luís Caires. Propositions-as-types and shared state. Proc. ACM Program. Lang., 5(ICFP):1-30, 2021. URL: https://doi.org/10.1145/3473584.
  38. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming (artifact). Dagstuhl Artifacts Ser., 3(2):03:1-03:2, 2017. URL: https://doi.org/10.4230/DARTS.3.2.3.
  39. Rob van Glabbeek and Peter Höfner. Progress, justness, and fairness. ACM Comput. Surv., 52(4):69:1-69:38, 2019. URL: https://doi.org/10.1145/3329125.
  40. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact