Document Open Access Logo

Separating Sessions Smoothly

Authors Simon Fowler , Wen Kokke, Ornela Dardha , Sam Lindley, J. Garrett Morris

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.36.pdf
  • Filesize: 0.87 MB
  • 18 pages

Document Identifiers

Author Details

Simon Fowler
  • University of Glasgow, UK
Wen Kokke
  • The University of Edinburgh, UK
Ornela Dardha
  • University of Glasgow, UK
Sam Lindley
  • The University of Edinburgh, UK
J. Garrett Morris
  • The University of Iowa, Iowa City, IA, USA

Funding

Work supported by EPSRC grants EP/K034413/1 (ABCD), EP/T014628/1 (STARDUST), EP/L01503X/1 (CDT PPar), ERC Consolidator Grant 682315 (Skye), UKRI Future Leaders Fellowship MR/T043830/1 (EHOP), a UK Government ISCF Metrology Fellowship grant, EU HORIZON 2020 MSCA RISE project 778233 (BehAPI), and NSF grant CCF-2044815.

Acknowledgements

We thank the anonymous reviewers for their helpful comments and suggestions.

Cite As Get BibTex

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating Sessions Smoothly. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.36

Abstract

This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Functional languages
  • Theory of computation → Linear logic
Keywords
  • session types
  • hypersequents
  • linear lambda calculus

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. Theoretical Computer Science, 135(1):5-9, 1994. Google Scholar
  2. Federico Aschieri and Francesco A. Genco. Par means parallel: multiplicative linear logic proofs as concurrent functional programs. Proc. ACM Program. Lang., 4(POPL):18:1-18:28, 2020. Google Scholar
  3. Robert Atkey, Sam Lindley, and J. Garrett Morris. Conflation confers concurrency. In A List of Successes That Can Change the World, volume 9600 of Lecture Notes in Computer Science, pages 32-55. Springer, 2016. Google Scholar
  4. Arnon Avron. Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell., 4:225-248, 1991. Google Scholar
  5. Gianluigi Bellin and Philip J. Scott. On the pi-calculus and linear logic. Theoretical Computer Science, 135(1):11-65, 1994. Google Scholar
  6. Michele Boreale. On the expressiveness of internal mobility in name-passing calculi. Theoretical Computer Science, 195(2):205-226, March 1998. URL: https://doi.org/10.1016/s0304-3975(97)00220-x.
  7. Luìs Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Proc. of CONCUR, volume 6269 of LNCS, pages 222-236. Springer, 2010. Google Scholar
  8. Marco Carbone, Ornela Dardha, and Fabrizio Montesi. Progress as compositional lock-freedom. In Proc. of COORDINATION, volume 8459 of Lecture Notes in Computer Science, pages 49-64. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43376-8_4.
  9. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence generalises duality: A logical explanation of multiparty session types. In CONCUR, volume 59 of LIPIcs, pages 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  10. Marco Carbone, Fabrizio Montesi, and Carsten Schürmann. Choreographies, logically. Distributed Comput., 31(1):51-67, 2018. Google Scholar
  11. Olivier Danvy, Kevin Millikin, and Lasse R. Nielsen. On one-pass CPS transformations. J. Funct. Program., 17(6):793-812, 2007. Google Scholar
  12. Ornela Dardha and Simon J. Gay. A new linear logic for deadlock-free session-typed processes. In Proc. of FoSSaCS, volume 10803 of LNCS, pages 91-109. Springer, 2018. Google Scholar
  13. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Inf. Comput., 256:253-286, 2017. Google Scholar
  14. Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. Exceptional asynchronous session types: session types without tiers. Proc. ACM Program. Lang., 3(POPL):28:1-28:29, 2019. Google Scholar
  15. Simon J. Gay and Rajagopal Nagarajan. Intensional and extensional semantics of dataflow programs. Formal Aspects of Computing, 15(4):299-318, 2003. Google Scholar
  16. Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19-50, 2010. Google Scholar
  17. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  18. Kohei Honda. Types for dyadic interaction. In CONCUR, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. Google Scholar
  19. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Proc. of ESOP, volume 1381 of LNCS, pages 122-138. Springer, 1998. Google Scholar
  20. Atsushi Igarashi, Peter Thiemann, Yuya Tsuda, Vasco T. Vasconcelos, and Philip Wadler. Gradual session types. J. Funct. Program., 29:e17, 2019. Google Scholar
  21. Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. Session type inference in Haskell. In Proc. of PLACES, volume 69 of EPTCS, pages 74-91, 2010. URL: https://doi.org/10.4204/EPTCS.69.6.
  22. Naoki Kobayashi. Type systems for concurrent programs. In Bernhard K. Aichernig and Tom Maibaum, editors, Formal Methods at the Crossroads. From Panacea to Foundational Support: 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002. Revised Papers, pages 439-453. Springer Berlin Heidelberg, 2003. URL: https://doi.org/10.1007/978-3-540-40007-3_26.
  23. Naoki Kobayashi. A new type system for deadlock-free processes. In Proc. of CONCUR, volume 4137 of LNCS, pages 233-247. Springer, 2006. Google Scholar
  24. Wen Kokke and Ornela Dardha. Deadlock-free session types in linear Haskell. CoRR, abs/2103.14481, 2021. Accepted for publication at the Haskell Symposium 2021. URL: http://arxiv.org/abs/2103.14481.
  25. Wen Kokke and Ornela Dardha. Prioritise the best variation. In FORTE, volume 12719 of Lecture Notes in Computer Science, pages 100-119. Springer, 2021. Google Scholar
  26. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: A fully-abstract semantics for classical processes. PACMPL, 3(POPL), 2019. Google Scholar
  27. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Taking linear logic apart. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Oxford, UK, 7-8 July 2018, volume 292 of Electronic Proceedings in Theoretical Computer Science, pages 90-103. Open Publishing Association, 2019. Google Scholar
  28. Jean-Jacques Lévy and Luc Maranget. Explicit substitutions and programming languages. In Foundations of Software Technology and Theoretical Computer Science, 1999, volume 1738 of LNCS. Springer, 1999. URL: https://doi.org/10.1007/3-540-46691-6_14.
  29. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. Comput., 185(2):182-210, 2003. Google Scholar
  30. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In Jan Vitek, editor, Programming Languages and Systems, pages 560-584. Springer Berlin Heidelberg, 2015. Google Scholar
  31. Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. SIGPLAN Not., 51(9):434-447, 2016. URL: https://doi.org/10.1145/3022670.2951921.
  32. Sam Lindley and J. Garrett Morris. Lightweight functional session types. In Simon Gay and Antonio Ravara, editors, Behavioural Types: from Theory to Tools, chapter 12, pages 265-286. River publishers, 2017. Google Scholar
  33. Fabrizio Montesi. Choreographic Programming. PhD thesis, IT University of Copenhagen, 2013. Google Scholar
  34. Fabrizio Montesi and Marco Peressotti. Classical transitions. CoRR, abs/1803.01049, 2018. URL: http://arxiv.org/abs/1803.01049.
  35. Dimitris Mostrous and Vasco T. Vasconcelos. Affine sessions. Log. Methods Comput. Sci., 14(4), 2018. Google Scholar
  36. Matthias Neubauer and Peter Thiemann. An implementation of session types. In Proc. of PADL, volume 3057 of Lecture Notes in Computer Science, pages 56-70. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24836-1_5.
  37. Dominic Orchard and Nobuko Yoshida. Session types with linearity in Haskell. Behavioural Types: from Theory to Tools, page 219, 2017. Google Scholar
  38. Dominic A. Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In Proc. of POPL, pages 568-581. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837634.
  39. Luca Padovani. Deadlock and Lock Freedom in the Linear π-Calculus. In Proc. of CSL-LICS, pages 72:1-72:10. ACM, 2014. Google Scholar
  40. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. Google Scholar
  41. Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In Proc. of Haskell. ACM, 2008. URL: https://doi.org/10.1145/1411286.1411290.
  42. John C. Reynolds. The meaning of types - from intrinsic to extrinsic semantics. Technical Report RS-00-32, BRICS, 2000. Google Scholar
  43. Matthew Sackman and Susan Eisenbach. Session types in Haskell: Updating message passing for the 21st century. Unpublished manuscript, 2008. Google Scholar
  44. Davide Sangiorgi. π-calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(1-2):235-274, 1996. URL: https://doi.org/10.1016/0304-3975(96)00075-8.
  45. Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. In Proc. of PARLE, volume 817 of LNCS, pages 398-413. Springer, 1994. Google Scholar
  46. Peter Thiemann and Vasco T. Vasconcelos. Label-dependent session types. Proceedings of the ACM on Programming Languages, 4(POPL):1-29, 2020. Google Scholar
  47. Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In ESOP, volume 7792 of Lecture Notes in Computer Science, pages 350-369. Springer, 2013. Google Scholar
  48. Vasco Vasconcelos, Antonio Ravara, and Simon J. Gay. Session types for functional multithreading. In CONCUR, volume 3170 of LNCS, pages 497-511. Springer, 2004. Google Scholar
  49. Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52-70, 2012. Google Scholar
  50. Vasco Thudichum Vasconcelos, Simon J. Gay, and Antonio Ravara. Type checking a multithreaded functional language with session types. Theor. Comput. Sci., 368(1-2):64-87, 2006. Google Scholar
  51. Philip Wadler. Propositions as sessions. Journal of Functional Programming, 24(2-3):384-418, 2014. Google Scholar
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