Ugo Dal Lago: On Type Systems for Termination and Complexity Analysis of Probabilistic Higher-Order Programs

Abstract: Probabilistic effects are algebraic and thus fit into the well-established Plotkin-Power abstract framework, through which operational semantics and algebraic theories can easily be derived. On the other hand, probabilistic termination and complexity analysis have a nature different from the one of their deterministic counterparts. This can be seen, as an example, when looking at these problems through the lenses of recursion theory. In this talk, we first of all clarify what it means for a probabilistic program to be terminating or to have bounded complexity, then focusing on some recently introduced type systems which guarantee almost sure termination of all typable terms, and which are obtained by adapting sized type and intersection type disciplines. We conclude the talk by showing how linear dependent types can be tuned so as to guarantee positive almost sure termination and average case complexity bounds.