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.

pdf

BibTeX:

@misc{Nipkow-Brinkop,
author={Tobias Nipkow and Hauke Brinkop},
title={Amortized Complexity Verified},year=2016,
note={Submitted for publication}}

Isabelle theories in the Archive of Formal Proofs

This is an extended version of this conference paper.