Termination of higher-order probabilistic programs

Higher-order probabilistic programming languages have recently been introduced as a way to describe probabilistic models, that may be used for instance in robotics or in machine learning, and these languages have been successful so far. The programs written in these languages are quite unusual: the fact that they are of higher-order means that they are built from functions, which can take themselves functions as arguments. I will explain in this talk how we can use type theory (a way to annotate the functions with the properties they satisfy) in a way which ensures that the typable programs terminate with probability 1 – or, in other words, have probability 0 to diverge. I will also explain how we can hope to capture more properties of higher-order probabilistic programs in the future using similar methods.