Paper Info
Title
Amortized Complexity Verified.
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.
Year
DOI
Venue
2015
10.1007/s10817-018-9459-3
ITP
Keywords
DocType
Volume
Amortized complexity, Interactive verification, Functional Programming
Conference
2014
Issue
ISSN
Citations 
3
1573-0670
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Tobias Nipkow13056232.28
Hauke Brinkop200.34