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.



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.