Skip Lists

Title:	Skip Lists
Authors:	Max W. Haslbeck and Manuel Eberl
Submission date:	2020-01-09
Abstract:	Skip lists are sorted linked lists enhanced with shortcuts and are an alternative to binary search trees. A skip lists consists of multiple levels of sorted linked lists where a list on level n is a subsequence of the list on level n − 1. In the ideal case, elements are skipped in such a way that a lookup in a skip lists takes O(log n) time. In a randomised skip list the skipped elements are choosen randomly. This entry contains formalized proofs of the textbook results about the expected height and the expected length of a search path in a randomised skip list.
BibTeX:	@article{Skip_Lists-AFP, author = {Max W. Haslbeck and Manuel Eberl}, title = {Skip Lists}, journal = {Archive of Formal Proofs}, month = jan, year = 2020, note = {\url{http://isa-afp.org/entries/Skip_Lists.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Monad_Normalisation
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.