Charles Grellois
INRIA Sophia-Antipolis
http://www.grellois.fr/
Date(s) : 21/09/2017 iCal
11 h 00 min - 12 h 00 min
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.
Catégories