Amortized Complexity Verified

DOI10.1007/978-3-319-22102-1_21zbMath1465.68059OpenAlexW2406041226MaRDI QIDQ2945642

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

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

Related Items (10)

Verified Root-Balanced Trees ⋮ Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation ⋮ Unnamed Item ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Amortized complexity verified ⋮ Verified analysis of random binary tree structures ⋮ Amortized Complexity ⋮ Automatic Functional Correctness Proofs for Functional Search Trees ⋮ Type-based analysis of logarithmic amortised complexity

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

Cites Work

• Unnamed Item
• The derivation of a tighter bound for top-down skew heaps
• The pairing heap: A new form of self-adjusting heap
• A systematic analysis of splaying
• Static prediction of heap space usage for first-order functional programs
• Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Amortized Computational Complexity
• Self-adjusting binary search trees
• Purely Functional Data Structures
• Self-Adjusting Heaps
• Parallel reductions in \(\lambda\)-calculus

This page was built for publication: Amortized Complexity Verified