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 the following non-trivial ones:
skew heaps, splay trees, splay heaps and pairing heaps.
The proofs are completely algebraic and are presented in some detail.
pdf
BibTeX:
@article{Nipkow-Brinkop,
author={Tobias Nipkow and Hauke Brinkop},
title={Amortized Complexity Verified},
journal={J. Automated Reasoning},volume=62,pages={367-391},year=2019}
Isabelle theories in the
Archive of Formal Proofs
This is an extended version of this conference paper.