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_ListsAFP,
author = {Max W. Haslbeck and Manuel Eberl},
title = {Skip Lists},
journal = {Archive of Formal Proofs},
month = jan,
year = 2020,
note = {\url{http://isaafp.org/entries/Skip_Lists.html},
Formal proof development},
ISSN = {2150914x},
}
