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.

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 report.