Amortized complexity verified

DOI10.1007/s10817-018-9459-3zbMath1465.68060OpenAlexW2934015820MaRDI QIDQ670702

Hauke Brinkop, Tobias Nipkow

Publication date: 20 March 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9459-3

zbMATH Keywords

functional programmingamortized complexityinteractive verification

Mathematics Subject Classification ID

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

Related Items

ATLAS: automated amortised complexity analysis of self-adjusting data structures, Exponential automatic amortized resource analysis

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• HOL
• OCaml
• CakeML
• ACE
• PairingHeap
• Splay Tree
• Skew Heap
• Amortized Complexity
• Archive Formal Proofs
• Root Balanced Tree

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• The derivation of a tighter bound for top-down skew heaps
• The pairing heap: A new form of self-adjusting heap
• Automatic average-case analysis of algorithms
• A systematic analysis of splaying
• Isabelle/HOL. A proof assistant for higher-order logic
• Automated higher-order complexity analysis
• Automated resource analysis with Coq proof objects
• A verified compiler from Isabelle/HOL to CakeML
• A Coq Library for Internal Verification of Running-Times
• Automatic Functional Correctness Proofs for Functional Search Trees
• Concrete Semantics
• 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
• Amortized Complexity Verified
• Denotational cost semantics for functional languages with inductive types
• Lightweight semiformal time complexity analysis for purely functional data structures
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Amortised Resource Analysis with Separation Logic
• Code Generation via Higher-Order Rewrite Systems
• Partial Recursive Functions in Higher-Order Logic
• Amortized Computational Complexity
• Self-adjusting binary search trees
• Automating program analysis
• Mechanical program analysis
• Purely Functional Data Structures
• Self-Adjusting Heaps
• Verified Root-Balanced Trees
• Resource bound certification
• Contract-based resource verification for higher-order functions with memoization
• Towards automatic resource bound analysis for OCaml
• CakeML
• Multivariate amortized resource analysis
• Implementation of Functional Languages
• Rank-Pairing Heaps