Bismuth has both data types for describing the type of a resource in a program (e.g., a variable) as well as session types which represent the communication protocols that programs use to communicate via channels with. The former of these is often represented by an uppercase T when referring to any data type. The latter is often represented by a P when referring to any session type. These are each ellaborated in their respective sections on this page.
The local process gets to determine which of the provided protocols (P_1, P_2, etc) to follow). Since 1.3.4, a unique label may prefix options in a choice to provide semantic meaning and allow duplicate protocols to exist within a choice.
The other process gets to determine which of the provided protocols (P_1, P_2, etc) to follow). Since 1.3.4, a unique label may prefix options in a choice to provide semantic meaning and allow duplicate protocols to exist within a choice.
Cancelable
Cancelable<P>
1.3.4
Allows the protocol P to be canceled by either party privy to the protocol at any time.