Amortized Complexity Verified
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.
pdf
BibTeX:
@inproceedings{Nipkow-ITP15,
author={Tobias Nipkow},
title={Amortized Complexity Verified},
booktitle={Interactive Theorem Proving (ITP 2015)},
editor={C. Urban and X. Zhang},
publisher=Springer,series=LNCS,volume={9236},pages={310-324},year=2015}
Isabelle theories in the
Archive of Formal Proofs
Extended journal version.