session type

Interaction between two processes can be checked using binary session types, while interactions between more than two processes can be checked using multiparty session types.{{cite book |last1=Honda |first1=Kohei |last2=Yoshida |first2=Nobuko |last3=Carbone |first3=Marco |title=Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages |chapter=Multiparty asynchronous session types |date=2008 |pages=273–284 |doi=10.1145/1328438.1328472|hdl=10044/1/26368 |isbn=9781595936899 |s2cid=53038488 |url=https://pure.itu.dk/portal/da/publications/f154b152-abd3-4f1e-a5d5-c0825f87ebd4 }} In multiparty session types interactions between all participants are described using a global type, which is then projected into local types that describe communication from the local view of each participant. Importantly, the global type encodes the sequencing information of the communication, which would be lost if we were to use binary session types to encode the same communication.{{cite conference |title=A Very Gentle Introduction to Multiparty Session Types |last1=Yoshida |first1=Nobuko |last2=Gheri |first2=Lorenzo |date=2019 |conference=ICDCIT 2020 |doi=10.1007/978-3-030-36987-3_5}}

Binary session types can be described using send operations ($!$), receive operations ($?$), branches (), selections ($\backslash oplus$), recursion ($rec$) and termination ($end$).

For example, $S\; =\; \backslash ;\; !bool.?int.end$ represents a session type $S$ which first sends a boolean ($!bool$), then receives an integer ($?int$) before finally terminating ($end$).

Session types have been adapted for several existing programming languages, including:

• lchannels (Scala){{cite web |title=Session programming in Scala |url=https://alcestes.github.io/lchannels/ |website=alcestes.github.io |access-date=2 November 2021 |language=en-us}}
• Effpi (Scala)
• STMonitor (Scala){{cite web |title=STMonitor |url=https://chrisbartoloburlo.github.io/stmonitor/ |website=chrisbartoloburlo.github.io |access-date=2 November 2021 |language=en}}
• EnsembleS{{cite journal |last1=Harvey |first1=Paul |last2=Fowler |first2=Simon |last3=Dardha |first3=Ornela |last4=Gay |first4=Simon J. |title=Multiparty Session Types for Safe Runtime Adaptation in an Actor Language |journal=35th European Conference on Object-Oriented Programming (ECOOP 2021) |date=2021 |volume=194 |pages=10:1–10:30 |doi=10.4230/LIPIcs.ECOOP.2021.10|doi-access=free |s2cid=234681015 }}
• Session-types (Rust){{cite book |last1=Jespersen |first1=Thomas Bracht Laumann |last2=Munksgaard |first2=Philip |last3=Larsen |first3=Ken Friis |title=Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming |chapter=Session types for Rust |series=WGP 2015 |date=30 August 2015 |pages=13–22 |doi=10.1145/2808098.2808100 |chapter-url=https://doi.org/10.1145/2808098.2808100 |publisher=Association for Computing Machinery|isbn=9781450338103 |s2cid=18320631}}
• sesh (Rust){{cite journal |last1=Kokke |first1=Wen |title=Rusty Variation: Deadlock-free Sessions with Failure in Rust |journal=Electronic Proceedings in Theoretical Computer Science |date=12 September 2019 |volume=304 |pages=48–60 |doi=10.4204/EPTCS.304.4 |arxiv=1909.05970 |s2cid=198166990 |url=https://doi.org/10.4204/EPTCS.304.4 |issn=2075-2180}}
• Session Actors (Python){{cite journal |last1=Yoshida |first1=Nobuko |last2=Neykova |first2=Rumyana |title=Multiparty Session Actors |journal=Logical Methods in Computer Science |date=29 March 2017 |volume=13 |issue=1 |doi=10.23638/LMCS-13(1:17)2017 |s2cid=65240382 |url=https://doi.org/10.23638/LMCS-13(1:17)2017 |language=en|arxiv=1609.05687 }}
• Monitored Session Erlang (Erlang){{cite journal |last1=Fowler |first1=Simon |title=An Erlang Implementation of Multiparty Session Actors |journal=Electronic Proceedings in Theoretical Computer Science |date=10 August 2016 |volume=223 |pages=36–50 |doi=10.4204/EPTCS.223.3 |arxiv=1608.03321 |s2cid=418549 |url=https://doi.org/10.4204/EPTCS.223.3 |issn=2075-2180}}
• FuSe (OCaml){{cite journal |last1=Padovani |first1=Luca |title=A simple library implementation of binary sessions |journal=Journal of Functional Programming |date=2017 |volume=27 |page=e4 |doi=10.1017/S0956796816000289 |hdl=2318/1634956 |s2cid=19776781 |url=https://doi.org/10.1017/S0956796816000289 |language=en |issn=0956-7968|hdl-access=free }}
• session-ocaml (OCaml){{cite journal |last1=Imai |first1=Keigo |last2=Yoshida |first2=Nobuko |last3=Yuen |first3=Shoji |title=Session-ocaml: A session-based library with polarities and lenses |journal=Science of Computer Programming |date=March 2019 |volume=172 |pages=135–159 |doi=10.1016/j.scico.2018.08.005 |s2cid=69673075 |language=en |issn=0167-6423|doi-access=free |hdl=10044/1/63748 |hdl-access=free }}{{cite web |title=Session OCaml |last1=Imai |first1=Keigo|url=https://www.ct.info.gifu-u.ac.jp/~keigoi/session-ocaml/ |website=www.ct.info.gifu-u.ac.jp |access-date=2 November 2021}}
• Priority Sesh (Haskell){{cite arXiv |last1=Kokke |first1=Wen |last2=Dardha |first2=Ornela |title=Deadlock-Free Session Types in Linear Haskell |date=26 March 2021 |class=cs.PL |eprint=2103.14481}}
• Java Typestate Checker (Java){{cite web |title=Java Typestate Checker |website=GitHub |url=https://github.com/jdmota/java-typestate-checker}}{{cite journal |last1=Bacchiani |first1=Lorenzo |last2=Bravetti |first2=Mario |last3=Giunti |first3=Marco |last4=Mota |first4=João |last5=Ravara |first5=António |title=A Java typestate checker supporting inheritance |journal=Sci. Comput. Program. |date=2022 |volume=221 |page=102844 |doi=10.1016/j.scico.2022.102844 |s2cid=250940803 |doi-access=free |hdl=10362/145315 |hdl-access=free }}{{cite book |last1=Mota |first1=João |last2=Giunti |first2=Marco |last3=Ravara |first3=António |chapter=Java Typestate Checker |title=Proceedings of COORDINATION 2021 |series=Lecture Notes in Computer Science |date=2021 |volume=12717 |pages=121–133 |doi=10.1007/978-3-030-78142-2_8 |isbn=978-3-030-78141-5 |s2cid=235383301 |chapter-url=https://doi.org/10.1007/978-3-030-78142-2_8}}
• Swift Sessions (Swift){{Cite web |last1=Rubicini |first1=Alessio |last2=Padovani |first2=Luca |date=2023 |title=Swift Sessions: a library implementation of binary session types in Swift |website=GitHub |url=https://github.com/alessiorubicini/SwiftSessions }}

{{reflist}}

{{DEFAULTSORT:Session types}}

Category:Concurrency (computer science)

Category:Type theory

Category:Type systems

{{Comp-sci-stub}}