### Abstract

Splay trees are self-adjusting binary search trees which were invented by Sleator and Tarjan [JACM 1985]. This entry provides executable and verified functional splay trees as well as the related splay heaps (due to Okasaki).

The amortized complexity of splay trees and heaps is analyzed in the AFP entry Amortized Complexity.

### License

BSD License

### History

July 12, 2016
  Moved splay heaps here from Amortized_Complexity

### Topics

- Computer science/Data structures

### Related publications

- Nipkow, T., & Brinkop, H. (2018). Amortized Complexity Verified. Journal of Automated Reasoning, 62(3), 367–391. https://doi.org/10.1007/s10817-018-9459-3
- Chapter Splay Trees in Functional Data Structures and Algorithms
- Wikipedia

### Session Splay_Tree

- Splay_Tree
- Splay_Map
- Splay_Heap

### Used by

- Amortized Complexity Verified

## Cite

×

Splay_Tree-AFP

    @article{Splay_Tree-AFP,
      author  = {Tobias Nipkow},
      title   = {Splay Tree},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Splay_Tree.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
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014