# 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.