Splay Tree

Tobias Nipkow 🌐

August 12, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Related publications

Session Splay_Tree

Used by

Cite

× 
@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: