Munksgaard/session-types

opposite of a Send with some type T is a Recv of type T.A channel of type Chan<E, Send<T, P>> implements the method send(T) → Chan<E, P>.A channel of type Chan<E, Recv<T, Q>> implements the method recv() → (T, Chan<E, Q>).There is the option of making choices in the protocol, for one process to choices.A channel of type Chan<E, Choose<P, Q>> implements two methods:that communicates the choice of protocols P and Q to the other process.A channel of type Chan<E, Offer<P, Q>> implements offer() → Branch<Chan<E, P>, Chan<E, Q>>. The type Rec<P> allows repeating the protocol P.A channel of type Chan<E, Rec<P>> implements the method enter() → Chan<(P, E), P>. Var<Z> points to the top of the stack.A channel of type Chan<(P, E), Var<Z>> implements the method zero() → Chan<(P, E), P>, ie Var<Z> is replaced by P at the top of the stack.The following program indefinitely sends some string:Protocols in the environment can also be popped from the stack with This requires there to be at least one protocol in the stack.A channel of type Chan<(P, E), Var<S<N>>> implements the method succ() -> Chan<E, Var<N>> that peels away the P from the environment and S in the