Verified analysis of random binary tree structures

DOI10.1007/978-3-319-94821-8_12zbMath1468.68288OpenAlexW2809929373MaRDI QIDQ5916263

Manuel Eberl, Tobias Nipkow, Max W. Haslbeck

Publication date: 4 October 2018

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

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_12

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Searching and sorting (68P10) Data structures (68P05) Randomized algorithms (68W20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Zip-zip trees: making zip trees more balanced, biased, compact, or persistent ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Verified analysis of random binary tree structures

Uses Software

• Coq
• Isabelle
• PRISM
• Isabelle/HOL
• Isar
• HOL
• Ergodic theory
• CryptHOL
• Amortized Complexity
• Archive Formal Proofs
• QuickSort Cost
• Treaps
• Root Balanced Tree
• Random BSTs
• Density Compiler

This page was built for publication: Verified analysis of random binary tree structures