Session type
≈ 2 min read
Names in other languages
No names in other languages are held for this entry yet.
Article bodies are English and are not machine-translated. A name in another language is not a translation of the article.
In type theory, session types are used to ensure correctness in concurrent programs. They guarantee that messages sent and received between concurrent programs are in the expected order and of the expected type. Session type systems have been adapted for both channel and actor systems. Session types are used to ensure desirable properties in concurrent and distributed systems, i.e. absence of communication errors or deadlocks, and protocol conformance.
In type theory, session types are used to ensure correctness in concurrent programs. They guarantee that messages sent and received between concurrent programs are in the expected order and of the expected type. Session type systems have been adapted for both channel and actor systems. Session types are used to ensure desirable properties in concurrent and distributed systems, i.e. absence of communication errors or deadlocks, and protocol conformance. For example, S = \; !bool.?int.end represents a session type S which first sends a boolean ( !bool ), then receives an integer ( ?int ) before finally terminating ( end ). ==Implementations== Session types have been adapted for several existing programming languages, including: lchannels (Scala) Effpi (Scala) STMonitor (Scala) EnsembleS Session-types (Rust) sesh (Rust) Session Actors (Python) Monitored Session Erlang (Erlang) FuSe (OCaml) session-ocaml (OCaml) Priority Sesh (Haskell) Java Typestate Checker (Java) Swift Sessions (Swift)
Text derived from https://en.wikipedia.org/w/index.php?oldid=1310016232 under CC BY-SA 4.0; modifications have been made.