Formal Verification of Higher-order Probabilistic Programs

Marco Gaboardi ( Boston University )

In this talk I will introduce a program logic for proving properties of probabilistic programs written in an expressive probabilistic higher-order language with continuous distributions and operators for conditioning distributions by real-valued functions. This program logics retains the comfortable reasoning style of informal proofs thanks to carefully selected axiomatizations of key results from probability theory. To show this, I will discuss the use of this program logic in the verification of several examples from statistics, probabilistic inference, machine learning, and differential privacy.