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.
On the Almost-Sure Termination of Binary Sessions
Dal Lago, Ugo;Padovani, Luca
2024-01-01
Abstract
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
