Intersection Types and (Positive) Almost-Sure Termination

Ugo Dal Lago, Claudia Faggian, Simona Ronchi Della Rocca

Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice…