On the Almost-Sure Termination of Binary Sessions

We investigate the termination problem in a calculus of sessions with probabilistic choices. In this setting, a whole range of termination properties can be defined, from the weaker almost-sure termination to strong almost-sure termination, passing through positive almost-sure termination. We present two similar session type systems closely related to classical linear logic with exponentials that guarantee the two extremal properties in such range. In both type systems, the definitional overhead that deals with the ensured termination property is kept to a minimum.