Amortized Complexity Verified
Author: Tobias Nipkow
Paper Information
| Title: | Amortized Complexity Verified |
| Authors: | Tobias Nipkow |
| Proceedings: | Isabelle 2014 Papers (Unrefereed) |
| Editors: | Tobias Nipkow, Lawrence Paulson and Makarius Wenzel |
| Keywords: | verification, amortized complexity, theorem proving |
| Abstract: | ABSTRACT. A framework for the analysis of the amortized complexity of (functional) data structures is formalized in Isabelle/HOL and applied to two non-trivial examples: skew heaps and splay trees. In the same spirit we show that the move-to-front algorithm for the list update problem is 2-competitive. |
| Pages: | 16 |
| Talk: | Jul 13 17:40 |
| Paper: |  |