Amortized Complexity Verified

Tobias Nipkow 🌐

July 7, 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

A framework for the analysis of the amortized complexity of functional data structures is formalized in Isabelle/HOL and applied to a number of standard examples and to the folowing non-trivial ones: skew heaps, splay trees, splay heaps and pairing heaps.

License

BSD License

History

July 14, 2016
Moved pairing heaps from here to the new Pairing_Heap
July 12, 2016
Moved splay heaps from here to Splay_Tree
March 17, 2015
Added pairing heaps by Hauke Brinkop.

Topics

Related publications

Session Amortized_Complexity

Depends on

Used by

Cite

× 
@article{Amortized_Complexity-AFP,
  author  = {Tobias Nipkow},
  title   = {Amortized Complexity Verified},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Amortized_Complexity.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: