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

### License

BSD License

### Topics

- Computer science/Data structures
- Computer science/Algorithms/Randomized

### Session Skip_Lists

- Pi_pmf
- Misc
- Geometric_PMF
- Skip_List

### Depends on

- Monad normalisation

### Used by

- The Schwartz-Zippel Lemma

### Auto-related entries

- Verifying Imperative Programs using Auto2
- Treaps

## Cite

×

Skip_Lists-AFP

    @article{Skip_Lists-AFP,
      author  = {Max W. Haslbeck and Manuel Eberl},
      title   = {Skip Lists},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Skip_Lists.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jan 10, 2020 : Isabelle2019