Amortized Complexity Verified

Tobias Nipkow and Hauke Brinkop

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},
year=2018,
note={Accepted for publication}}

Isabelle theories in the Archive of Formal Proofs

This is an extended version of this conference paper.