Automatic Functional Correctness Proofs for Functional Search Trees

DOI10.1007/978-3-319-43144-4_19zbMath1478.68065OpenAlexW2483569599MaRDI QIDQ2829265

Tobias Nipkow

Publication date: 27 October 2016

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

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_19

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Verified Root-Balanced Trees, Automatic refinement to efficient data structures: a comparison of two approaches, A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL, Unnamed Item, Amortized complexity verified, An assertional proof of red-black trees using Dafny, Verified analysis of random binary tree structures, Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code

Uses Software

• ACL2
• Isabelle
• Isabelle/HOL
• HOL
• Splay Tree
• AVL trees
• Amortized Complexity
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL
• Balanced trees with removals: An exercise in rewriting and proof
• Isabelle/HOL. A proof assistant for higher-order logic
• Symmetric binary B-trees: Data structure and maintenance algorithms
• Proof of correctness of data representations
• Red-black trees with types
• Concrete Semantics
• Amortized Complexity Verified
• Purely Functional 1-2 Brother Trees
• Self-adjusting binary search trees
• 1-2 Brother Trees or AVL Trees Revisited
• Programming with Equations
• Purely Functional Data Structures
• Programming Languages and Systems
• Data Refinement in Isabelle/HOL