Abstract:

Probabilistic programs, that is, programs that use randomness in their execution, appear everywhere in modern computing. For example, in randomized algorithms, where randomization is used to increase efficiency, or in cryptography, where it is used to ensure security. Although the principles that make these algorithms and protocols work are generally well-understood, these programs are ultimately written in industrial languages, and the interaction between randomization and the rest of the language features makes these critical programs hard to reason about. In this talk, I will present my work, which focuses on developing formal methods and tools to reason about probabilistic programs written in realistic programming languages. These techniques have been implemented in the proof assistant Rocq, which both gives us strong correctness guarantees, and also allows us to scale them up beyond the scope of previous work.