Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Randomised Binary Search Trees


view this post on Zulip Email Gateway (Aug 22 2022 at 18:39):

From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce another AFP entry contributed by Manuel Eberl: Randomised Binary Search Trees

"This work is a formalisation of the Randomised Binary Search Trees introduced by Martínez and Roura, including definitions and correctness proofs.

Like randomised treaps, they are a probabilistic data structure that behaves exactly as if elements were inserted into a non-balancing BST in random order. However, unlike treaps, they only use discrete probability distributions, but their use of randomness is more complicated."

It's a wonderful demonstration of what can be done with the libraries now our disposal, including probability theory and a number of theories related to the analysis of algorithms.

It is now online at https://www.isa-afp.org/entries/Randomised_BSTs.html

Larry Paulson


Last updated: Mar 29 2024 at 12:28 UTC