Amortized complexity verified

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

18 Scopus citations

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 three famous non-trivial ones: skew heaps, splay trees and splay heaps.

Original languageEnglish
Title of host publicationInteractive Theorem Proving - 6th International Conference, ITP 2015, Proceedings
EditorsXingyuan Zhang, Christian Urban
PublisherSpringer Verlag
Pages310-324
Number of pages15
ISBN (Print)9783319221014
DOIs
StatePublished - 2015
Event6th International Conference on Interactive Theorem Proving, ITP 2015 - Nanjing, China
Duration: 24 Aug 201527 Aug 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9236
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th International Conference on Interactive Theorem Proving, ITP 2015
Country/TerritoryChina
CityNanjing
Period24/08/1527/08/15

Fingerprint

Dive into the research topics of 'Amortized complexity verified'. Together they form a unique fingerprint.

Cite this