Amortized Complexity Verified

Tobias Nipkow

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 three famous non-trivial ones: skew heaps, splay trees and splay heaps.



author={Tobias Nipkow},
title={Amortized Complexity Verified},
booktitle={Interactive Theorem Proving (ITP 2015)},
editor={C. Urban and X. Zhang},

Isabelle theories in the Archive of Formal Proofs

Extended report.