Probabilistic Functional Programs: Termination and Verification

General presentation of the topic. Functional programming is a successful paradigm originating in λ-calculus. It has led to the development of programming languages such as OCaml and Haskell. On the other hand, probabilistic computation is more and more used nowadays, in cryptography, robotics or for machine learning-related approaches. Both approaches have been combined in languages such as Church [2] or Anglican [5]. We propose to study termination and verification problems for probabilistic λ-calculi, which mix functional programming with probabilistic programming.