Email Gateway (Jun 29 2023 at 10:46): Email Gateway (Jun 29 2023 at 10:46):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new contribution, Executable Randomized Algorithms, by Emin Karayel and Manuel Eberl.
Abstract
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.
I’ve always found probabilistic algorithms to be paradoxical and the idea of their verification more so. (It was first tackled here at Cambridge by Joe Hurd, a student of Mike Gordon, in 2003.) This new approach introduces executability.
It’s on-line at https://www.isa-afp.org/entries/Executable_Randomized_Algorithms.html
Larry Paulson
Last updated: Apr 29 2024 at 01:08 UTC