Abstract
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 folowing non-trivial ones: skew heaps,
splay trees, splay heaps and pairing heaps.
BSD LicenseA preliminary version of this work (without pairing heaps) is described in a paper published in the proceedings of the conference on Interactive Theorem Proving ITP 2015. An extended version of this publication is available here.
Change history
[2015-03-17] Added pairing heaps by Hauke Brinkop.
[2016-07-12] Moved splay heaps from here to Splay_Tree
[2016-07-14] Moved pairing heaps from here to the new Pairing_Heap
Depends On
Used by
Topics
Related Entries
Theories
- Amortized_Framework0
- Amortized_Framework
- Amortized_Examples
- Priority_Queue_ops_merge
- Skew_Heap_Analysis
- Lemmas_log
- Splay_Tree_Analysis_Base
- Splay_Tree_Analysis
- Splay_Tree_Analysis_Optimal
- Priority_Queue_ops
- Splay_Heap_Analysis
- Pairing_Heap_Tree_Analysis
- Pairing_Heap_Tree_Analysis2
- Pairing_Heap_List1_Analysis
- Pairing_Heap_List1_Analysis2
- Pairing_Heap_List2_Analysis