Amortized complexity verified

DOI10.1007/978-3-319-22102-1_21MaRDI QIDQ2945642zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-22102-1_21

Mathematics Subject Classification ID

Data structures (68P05) Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Amortized complexity verified
• scientific article; zbMATH DE number 54254
• ATLAS: automated amortised complexity analysis of self-adjusting data structures
• Type-based analysis of logarithmic amortised complexity
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation

Cites work

• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• A systematic analysis of splaying
• Amortized Computational Complexity
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Parallel reductions in \(\lambda\)-calculus
• Purely Functional Data Structures
• Self-Adjusting Heaps
• Self-adjusting binary search trees
• Static prediction of heap space usage for first-order functional programs
• The derivation of a tighter bound for top-down skew heaps
• The pairing heap: A new form of self-adjusting heap
• Verifying Nonlinear Real Formulas Via Sums of Squares

Cited in

(14)

• Amortized Computational Complexity
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• ATLAS: automated amortised complexity analysis of self-adjusting data structures
• Automatic functional correctness proofs for functional search trees
• scientific article; zbMATH DE number 54254 (Why is no real title available?)
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Amortized Complexity
• Verified analysis of random binary tree structures
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Verified Root-Balanced Trees
• Amortized complexity verified
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Type-based analysis of logarithmic amortised complexity
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

Describes a project that uses

Uses Software

• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: Amortized complexity verified

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945642)