Demonstration of proving probabilistic programs using theorem proving
Based on the theory of probabilistic relations and its implementation in Isabelle/UTP
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.
Kangfeng (Randall) Ye
Research Associate (Computer Science)
My research interests include probabilistic modelling and verification using formal specification and verification (both model checking and theorem proving) and model-based engineering.