Demonstration of proving probabilistic programs using theorem proving
Based on the theory of probabilistic relations and its implementation in Isabelle/UTP
![](/~ky582/showcase/demonstration_of_probabilistic_relation/featured_hu7888d7cc804f4e8e895bb066cdd171ef_1109337_720x2500_fit_q75_h2_lanczos_3.webp)
Here we illustrate a probabilistic programming language that we are developing, its semantic implementation in Isabelle/UTP (UTP in Isabelle/HOL), the introduced Iverson bracket and distribution notations, proved algebraic laws including fixed-point theorems, reasoning about three probabilistic examples: a coin flip, the Monty Hall problem with learning facts, and a robot localisation.
The Isabelle/HOL theories for probabilistic relations can be found here.