Exposés

11:00: Charles Grellois (LSIS, Aix-Marseille), Two Type-Theoretic Approaches to Probabilistic Termination

A fundamental result in lambda-calculus states that terms that admit a simple type are strongly normalizing: in other words, they always terminate. The simply-typed lambda-calculus can be enriched with a recursion operator and, in this case, terms admitting a sized type always terminate. In this talk, we study a simply-typed lambda-calculus enhanced with a recursion operator and a probabilistic choice operator, and we focus on the probabilistic counterpart of termination: almost-sure termination (AST), that is, termination with probability 1. I will explain how the sized types approach can be extended to the probabilistic setting, so that we obtain a type system in which typability guarantees AST. I will then sketch ongoing work on a more powerful approach using dependent types, in order to capture AST for a wider class of programs. This is joint work with Dal Lago.