Session type

Session types are used to ensure desirable properties in concurrent and distributed systems, i.e. absence of communication errors or deadlocks, and protocol conformance.

Binary versus multiparty session types

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. 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.