Amortized complexity verified

DOI10.1007/S10817-018-9459-3zbMATH Open1465.68060OpenAlexW2934015820MaRDI QIDQ670702FDOQ670702

Authors: Tobias Nipkow, Hauke Brinkop 

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

Recommendations

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

zbMATH Keywords

functional programmingamortized complexityinteractive verification

Mathematics Subject Classification ID

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

Cites Work

• Amortized Complexity Verified
• Title not available (Why is that?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Self-adjusting binary search trees
• Multivariate amortized resource analysis
• Title not available (Why is that?)
• Concrete Semantics
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Self-Adjusting Heaps
• CakeML
• The derivation of a tighter bound for top-down skew heaps
• Partial Recursive Functions in Higher-Order Logic
• Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
• The pairing heap: A new form of self-adjusting heap
• Purely Functional Data Structures
• Code generation via higher-order rewrite systems
• Amortized Computational Complexity
• Mechanical program analysis
• Implementation of Functional Languages
• Automatic average-case analysis of algorithms
• A systematic analysis of splaying
• 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
• Static prediction of heap space usage for first-order functional programs
• Denotational cost semantics for functional languages with inductive types
• Lightweight semiformal time complexity analysis for purely functional data structures
• Amortised resource analysis with separation logic
• Automating program analysis
• Title not available (Why is that?)
• Verified Root-Balanced Trees
• Resource bound certification
• Contract-based resource verification for higher-order functions with memoization
• Towards automatic resource bound analysis for OCaml
• Rank-pairing heaps
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

Cited In (6)

• ATLAS: automated amortised complexity analysis of self-adjusting data structures
• Title not available (Why is that?)
• Exponential automatic amortized resource analysis
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Type-based analysis of logarithmic amortised complexity
• Amortized Computational Complexity

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

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 Q670702)