Splay Tree

Tobias Nipkow

12 August 2014

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.

BSD License

Change history

[2016-07-12] Moved splay heaps here from Amortized_Complexity

Used by

Topics

Related Entries

Theories

Cite

×
@article{Splay_Tree-AFP,
  author  = {Tobias Nipkow},
  title   = {Splay Tree},
  journal = {Archive of Formal Proofs},
  month   = August,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Splay_Tree.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download