Executable Randomized Algorithms

Emin Karayel 📧 and Manuel Eberl 📧

June 19, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


In Isabelle, randomized algorithms are usually represented using probability mass functions (PMFs), with which it is possible to verify their correctness, particularly properties about the distribution of their result. However, that approach does not provide a way to generate executable code for such algorithms. In this entry, we introduce a new monad for randomized algorithms, for which it is possible to generate code and simultaneously reason about the correctness of randomized algorithms. The latter works by a Scott-continuous monad morphism between the newly introduced random monad and PMFs. On the other hand, when supplied with an external source of random coin flips, the randomized algorithms can be executed.


BSD License


Session Executable_Randomized_Algorithms