Amortized Complexity Verified

Tobias Nipkow; Hauke Brinkop

doi:10.1007/s10817-018-9459-3

Amortized Complexity Verified

Tobias Nipkow, Hauke Brinkop

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Contribution to journal › Article › peer-review

15 Scopus citations

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	https://doi.org/10.1007/s10817-018-9459-3
State	Published - 15 Mar 2019

Keywords

Amortized complexity
Functional Programming
Interactive verification

Access to Document

10.1007/s10817-018-9459-3

Cite this

@article{ee758ccd03154662ae251f7637c8587b,

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.",

keywords = "Amortized complexity, Functional Programming, Interactive verification",

author = "Tobias Nipkow and Hauke Brinkop",

note = "Publisher Copyright: {\textcopyright} 2018, Springer Science+Business Media B.V., part of Springer Nature.",

year = "2019",

month = mar,

day = "15",

doi = "10.1007/s10817-018-9459-3",

language = "English",

volume = "62",

pages = "367--391",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "3",

}

TY - JOUR

T1 - Amortized Complexity Verified

AU - Nipkow, Tobias

AU - Brinkop, Hauke

PY - 2019/3/15

Y1 - 2019/3/15

N2 - 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.

AB - 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.

KW - Amortized complexity

KW - Functional Programming

KW - Interactive verification

UR - http://www.scopus.com/inward/record.url?scp=85043722317&partnerID=8YFLogxK

U2 - 10.1007/s10817-018-9459-3

DO - 10.1007/s10817-018-9459-3

M3 - Article

AN - SCOPUS:85043722317

SN - 0168-7433

VL - 62

SP - 367

EP - 391

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 3

ER -

Amortized Complexity Verified

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this