Document Open Access Logo

Session Subtyping and Multiparty Compatibility Using Circular Sequents

Author Ross Horne

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.12.pdf
  • Filesize: 0.74 MB
  • 22 pages

Document Identifiers

Author Details

Ross Horne
  • Computer Science, University of Luxembourg, Esch-sur-Alzette, Luxembourg

Acknowledgements

This paper benefits hugely from discussions with Mariangiola Dezani-Ciancaglini and Paola Giannini who suggested restricting to a regular calculus.

Cite As Get BibTex

Ross Horne. Session Subtyping and Multiparty Compatibility Using Circular Sequents. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.12

Abstract

We present a structural proof theory for multi-party sessions, exploiting the expressive power of non-commutative logic which can capture explicitly the message sequence order in sessions. The approach in this work uses a more flexible form of subtyping than standard, for example, allowing a single thread to be substituted by multiple parallel threads which fulfil the role of the single thread. The resulting subtype system has the advantage that it can be used to capture compatibility in the multiparty setting (addressing limitations of pairwise duality). We establish standard results: that the type system is algorithmic, that multiparty compatible processes which are race free are also deadlock free, and that subtyping is sound with respect to the substitution principle. Interestingly, each of these results can be established using cut elimination. We remark that global types are optional in this approach to typing sessions; indeed we show that this theory can be presented independently of the concept of global session types, or even named participants.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
  • Theory of computation → Process calculi
Keywords
  • session types
  • subtyping
  • compatibility
  • linear logic
  • deadlock freedom

Metrics

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

References

  1. Samson Abramsky. Computational interpretations of linear logic. Theoretical computer science, 111(1):3-57, 1993. URL: https://doi.org/10.1016/0304-3975(93)90181-R.
  2. Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Trans. Program. Lang. Syst., 15(4):575-631, September 1993. URL: https://doi.org/10.1145/155183.155231.
  3. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. URL: https://doi.org/10.1093/logcom/2.3.297.
  4. 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), volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  5. Franco Barbanera and Ugo de'Liguoro. Sub-behaviour relations for session-based client/server systems. Mathematical Structures in Computer Science, 25(6):1339-1381, 2015. URL: https://doi.org/10.1017/S096012951400005X.
  6. Franco Barbanera and Mariangiola Dezani-Ciancaglini. Open multiparty sessions. In Proceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019., pages 77-96, 2019. URL: https://doi.org/10.4204/EPTCS.304.6.
  7. Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:10)2016.
  8. Eduardo Bonelli and Adriana Compagnoni. Multipoint session types for a distributed calculus. In Gilles Barthe and Cédric Fournet, editors, Trustworthy Global Computing, pages 240-256. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78663-4_17.
  9. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, October 2010. URL: https://doi.org/10.1093/logcom/exq052.
  10. Paola Bruscoli. A purely logical account of sequentiality in proof search. In Peter J. Stuckey, editor, Logic Programming, pages 302-316. Springer, 2002. URL: https://doi.org/10.1007/3-540-45619-8_21.
  11. Luís Caires and Jorge A. Pérez. Multiparty session types within a canonical binary theory, and beyond. In FORTE 2016, pages 74-95, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_6.
  12. Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty session types as coherence proofs. Acta Informatica, 54(3):243-269, 2017. URL: https://doi.org/10.1007/s00236-016-0285-y.
  13. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Ross Horne. Global types with internal delegation. Theoretical Computer Science, 807:128-153, 2020. URL: https://doi.org/10.1016/j.tcs.2019.09.027.
  14. Tzu-chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. Logical Methods in Computer Science, Volume 13, Issue 2, 2017. URL: https://doi.org/10.23638/LMCS-13(2:12)2017.
  15. Gabriel Ciobanu and Ross Horne. Behavioural analysis of sessions using the calculus of structures. In Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, pages 91-106, 2015. URL: https://doi.org/10.1007/978-3-319-41579-6_8.
  16. Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu. Intersection types and runtime errors in the pi-calculus. Proc. ACM Program. Lang., 3(POPL), 2019. URL: https://doi.org/10.1145/3290320.
  17. Rocco De Nicola and Matthew Hennessy. CCS without τ’s. In Hartmut Ehrig, Robert Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT '87, pages 138-152. Springer, 1987. URL: https://doi.org/10.1007/3-540-17660-8_53.
  18. Romain Demangeon and Kohei Honda. Full abstraction in a subtyped pi-calculus with linear types. In CONCUR, volume 6901 of LNCS, pages 280-296. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_19.
  19. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In Helmut Seidl, editor, Programming Languages and Systems, pages 194-213. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_10.
  20. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In Automata, Languages, and Programming, pages 174-186. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  21. Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:6)2012.
  22. Farzaneh Derakhshan and Frank Pfenning. Circular proof as session-typed processes: a local validity condition. CoRR, 2019. URL: http://arxiv.org/abs/1908.01909.
  23. Simon 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.
  24. Simon J. Gay and Malcolm Hole. Types and subtypes for client-server interactions. In ESOP, volume 1576 of Lecture Notes in Computer Science, pages 74-90. Springer, 1999. URL: https://doi.org/10.1007/3-540-49099-X_6.
  25. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. J. Log. Algebr. Meth. Program., 104:127-173, 2019. URL: https://doi.org/10.1016/j.jlamp.2018.12.002.
  26. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-112, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  27. Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In Hartmut Ehrig, Robert Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT '87, pages 52-66. Springer, 1987. URL: https://doi.org/10.1007/BFb0014972.
  28. Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Compututational Logic, 8, 2007. URL: https://doi.org/10.1145/1182613.1182614.
  29. Dick Hardt. The OAuth 2.0 authorization framework. standard rfc6749, Internet Engineering Task Force, 2012. URL: https://tools.ietf.org/html/rfc6749.
  30. Kohei Honda. Types for dyadic interaction. In CONCUR'93, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  31. Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida. Scribbling interactions with a formal foundation. In Raja Natarajan and Adegboyega Ojo, editors, Distributed Computing and Internet Technology, pages 55-75. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19056-8_4.
  32. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  33. 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.
  34. Ross Horne. The consistency and complexity of multiplicative additive system virtual. Scientific Annals of Computer Science, 25(2):245-316, 2015. URL: https://doi.org/10.7561/SACS.2015.2.245.
  35. Ross Horne. The sub-additives: A proof theory for probabilistic choice extending linear logic. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, pages 23:1-23:16, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.23.
  36. Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. Mathematical Structures in Computer Science, 29(8):1275–1308, 2019. URL: https://doi.org/10.1017/S0960129518000452.
  37. Naoki Kobayashi. A type system for lock-free processes. Information and Computation, 177(2):122-159, 2002. URL: https://doi.org/10.1016/S0890-5401(02)93171-8.
  38. Julien Lange and Emilio Tuosto. Synthesising choreographies from local session types. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory, pages 225-239. Springer, 2012. Google Scholar
  39. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 221-232. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676964.
  40. Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, page 434–447. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951921.
  41. Barbara Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6):1811-1841, 1994. URL: https://doi.org/10.1145/197320.197383.
  42. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51(1):125-157, 1991. URL: https://doi.org/10.1016/0168-0072(91)90068-W.
  43. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global principal typing in partially commutative asynchronous sessions. In Programming Languages and Systems, pages 316-332. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_23.
  44. Luca Padovani. Session types = intersection types + union types. In Proceedings Fifth Workshop on Intersection Types and Related Systems, ITRS 2010, Edinburgh, U.K., 9th July 2010., pages 71-89, 2010. URL: https://doi.org/10.4204/EPTCS.45.6.
  45. Luca Padovani. On projecting processes into session types. Mathematical Structures in Computer Science, 22(2):237–289, 2012. URL: https://doi.org/10.1017/S0960129511000405.
  46. Luca Padovani. Deadlock and lock freedom in the linear pi-calculus. In CSL-LICS, pages 72:1-72:10. ACM Press, 2014. URL: https://doi.org/10.1145/2603088.2603116.
  47. Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-453, 1996. URL: https://doi.org/10.1017/S096012950007002X.
  48. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. PACMPL, 3(POPL):30:1-30:29, 2019. URL: https://doi.org/10.1145/3290343.
  49. Paula Severi and Mariangiola Dezani-Ciancaglini. Observational equivalence for multiparty sessions. Fundam. Inform., 170(1-3):267-305, 2019. URL: https://doi.org/10.3233/FI-2019-1863.
  50. Alwen Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science, 2(2), 2006. URL: https://doi.org/10.2168/LMCS-2(2:4)2006.
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