Abstract
A framework for the analysis of the amortized complexity of functional data structures is formalized in the proof assistant 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.
| Original language | English |
|---|---|
| Pages (from-to) | 367-391 |
| Number of pages | 25 |
| Journal | Journal of Automated Reasoning |
| Volume | 62 |
| Issue number | 3 |
| DOIs | |
| State | Published - 15 Mar 2019 |
Keywords
- Amortized complexity
- Functional Programming
- Interactive verification
Fingerprint
Dive into the research topics of 'Amortized Complexity Verified'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver