Document Open Access Logo

A Self-Dual Distillation of Session Types

Author Jules Jacobs

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.23.pdf
  • Filesize: 0.84 MB
  • 22 pages

Document Identifiers

Author Details

Jules Jacobs
  • Radboud University Nijmegen, The Netherlands

Acknowledgements

I thank Robbert Krebbers, Stephanie Balzer, Jorge Pérez, Dan Frumin, Bas van den Heuvel, Anton Golov, Ike Mulder, and last but not least, the anonymous reviewers for the helpful discussions and feedback.

Cite As Get BibTex

Jules Jacobs. A Self-Dual Distillation of Session Types. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ECOOP.2022.23

Abstract

We introduce ƛ ("lambda-barrier"), a minimal extension of linear λ-calculus with concurrent communication, which adds only a single new fork construct for spawning threads. It is inspired by GV, a session-typed functional language also based on linear λ-calculus. Unlike GV, ƛ strives to be as simple as possible, and adds no new operations other than fork, no new type formers, and no explicit definition of session type duality. Instead, we use linear function function type τ₁ -∘ τ₂ for communication between threads, which is dual to τ₂ -∘ τ₁, i.e., the function type constructor is dual to itself. Nevertheless, we can encode session types as ƛ types, GV’s channel operations as ƛ terms, and show that this encoding is type-preserving. The linear type system of ƛ ensures that all programs are deadlock-free and satisfy global progress, which we prove in Coq. Because of ƛ’s minimality, these proofs are simpler than mechanized proofs of deadlock freedom for GV.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming languages
Keywords
  • Linear types
  • concurrency
  • lambda calculus
  • session types

Metrics

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

Supplementary Materials

References

  1. Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The Essence of Dependent Object Types, pages 249-272. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_14.
  2. Alen Arslanagic, Jorge A. Pérez, and Erik Voogd. Minimal Session Types (Pearl). In ECOOP 2019, 2019. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.23.
  3. Federico Aschieri, Agata Ciabattoni, and Francesco A. Genco. Gödel logic: From natural deduction to parallel computation. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005076.
  4. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222-236, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  5. Marco Carbone and Søren Debois. A graphical approach to progress for structured communication in web services. In ICE, volume 38 of EPTCS, pages 13-27, 2010. URL: https://doi.org/10.4204/EPTCS.38.4.
  6. Karl Crary, Robert Harper, and Sidd Puri. What is a recursive module? In PLDI, pages 50-63. ACM, 1999. URL: https://doi.org/10.1145/301618.301641.
  7. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In PPDP'12, 2012. URL: https://doi.org/10.1145/2370776.2370794.
  8. 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.
  9. Matthias Felleisen. On the expressive power of programming languages. Science of Computer Programming, 17(1):35-75, 1991. URL: https://doi.org/10.1016/0167-6423(91)90036-W.
  10. Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. In CONCUR, volume 203 of LIPIcs, pages 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.36.
  11. Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. Exceptional asynchronous session types: Session types without tiers. PACMPL, 3(POPL):28:1-28:29, 2019. URL: https://doi.org/10.1145/3290341.
  12. Simon J. Gay, Peter Thiemann, and Vasco T. Vasconcelos. Duality of session types: The final cut. In PLACES, volume 314 of EPTCS, pages 23-33, 2020. URL: https://doi.org/10.4204/EPTCS.314.3.
  13. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. JFP, 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  14. Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Information and Computation, 208(9):1031-1053, 2010. URL: https://doi.org/10.1016/j.ic.2010.05.002.
  15. Kohei Honda. Types for dyadic interaction. In CONCUR, volume 715 of LNCS, pages 509-523, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  16. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, volume 1381 of LNCS, pages 122-138, 1998. URL: https://doi.org/10.1007/BFb0053567.
  17. Jules Jacobs. Coq mechanization of lambda-barrier, 2021. The most recent version is at https://github.com/julesjacobs/cgraphs. URL: https://doi.org/https://zenodo.org/record/6560443.
  18. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang., 6(POPL):1-33, 2022. URL: https://doi.org/10.1145/3498662.
  19. Naoki Kobayashi. Type systems for concurrent programs. In 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, volume 2757 of Lecture Notes in Computer Science, pages 439-453, 2002. URL: https://doi.org/10.1007/978-3-540-40007-3_26.
  20. Wen Kokke and Ornela Dardha. Deadlock-free session types in linear haskell. In Haskell 2021: Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell, Virtual Event, Korea, August 26-27, 2021, Haskell 2021, 2021. URL: https://doi.org/10.1145/3471874.3472979.
  21. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In ESOP, volume 9032 of LNCS, pages 560-584, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_23.
  22. Sam Lindley and J. Garrett Morris. Embedding session types in Haskell. In Haskell Symposium, pages 133-145, 2016. URL: https://doi.org/10.1145/2976002.2976018.
  23. Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. In ICFP, pages 434-447, 2016. URL: https://doi.org/10.1145/2951913.2951921.
  24. Sam Lindley and J. Garrett Morris. Lightweight functional session types. In Behavioural Types: from Theory to Tools. River Publishers, 2017. Google Scholar
  25. Magnus O. Myreen and Scott Owens. Proof-producing synthesis of ml from higher-order logic. SIGPLAN Not., pages 115-126, 2012. URL: https://doi.org/10.1145/2398856.2364545.
  26. Joachim Niehren, Jan Schwinghammer, and Gert Smolka. A concurrent lambda calculus with futures. In Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings, volume 3717 of Lecture Notes in Computer Science, pages 248-263, 2005. URL: https://doi.org/10.1007/11559306_14.
  27. Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. URL: https://doi.org/10.1017/S0956796816000289.
  28. Joachim Parrow. Trios in concert. In Proof, Language and Interaction: Essays in Honour of Robin Milner, pages 621-637. MIT Press, 1998. Google Scholar
  29. Eric Roberts. An overview of minijava. SIGCSE Bull., 2001. URL: https://doi.org/10.1145/366413.364525.
  30. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in scala. In 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy, volume 56 of LIPIcs, pages 21:1-21:28, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  31. Philip Wadler. Propositions as sessions. In ICFP, pages 273-286, 2012. URL: https://doi.org/10.1145/2364527.2364568.
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