Séminaire, 21 septembre 2017
Exposés
 11:00: Charles Grellois (LSIS, AixMarseille), Two TypeTheoretic Approaches to Probabilistic Termination

A fundamental result in lambdacalculus states that terms that admit a simple type are strongly normalizing: in other words, they always terminate. The simplytyped lambdacalculus can be enriched with a recursion operator and, in this case, terms admitting a sized type always terminate. In this talk, we study a simplytyped lambdacalculus enhanced with a recursion operator and a probabilistic choice operator, and we focus on the probabilistic counterpart of termination: almostsure 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.