Amortized complexity verified (Q670702): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CakeML
@@ Property / describes a project that uses: CakeML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/Isar
@@ Property / describes a project that uses: Isabelle/Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OCaml
@@ Property / describes a project that uses: OCaml / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACE
@@ Property / describes a project that uses: ACE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Skew Heap
@@ Property / describes a project that uses: Skew Heap / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Splay Tree
@@ Property / describes a project that uses: Splay Tree / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PairingHeap
@@ Property / describes a project that uses: PairingHeap / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Amortized Complexity
@@ Property / describes a project that uses: Amortized Complexity / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Root Balanced Tree
@@ Property / describes a project that uses: Root Balanced Tree / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-018-9459-3
+Normal rank
@@ Property / OpenAlex ID @@
+W2934015820
@@ Property / OpenAlex ID: W2934015820 / rank @@
+Normal rank
@@ Property / cites work @@
+Amortised Resource Analysis with Separation Logic
@@ Property / cites work: Amortised Resource Analysis with Separation Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Automated higher-order complexity analysis
@@ Property / cites work: Automated higher-order complexity analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Automated resource analysis with Coq proof objects
+Normal rank
@@ Property / cites work @@
+Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
+Normal rank
@@ Property / cites work @@
+Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
+Normal rank
@@ Property / cites work @@
+Q3619797
@@ Property / cites work: Q3619797 / rank @@
+Normal rank
@@ Property / cites work @@
+Resource bound certification
@@ Property / cites work: Resource bound certification / rank @@
+Normal rank
@@ Property / cites work @@
+Lightweight semiformal time complexity analysis for purely functional data structures
+Normal rank
@@ Property / cites work @@
+Denotational cost semantics for functional languages with inductive types
+Normal rank
@@ Property / cites work @@
+Automatic average-case analysis of algorithms
@@ Property / cites work: Automatic average-case analysis of algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+The pairing heap: A new form of self-adjusting heap
+Normal rank
@@ Property / cites work @@
+Rank-Pairing Heaps
@@ Property / cites work: Rank-Pairing Heaps / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Nonlinear Real Formulas Via Sums of Squares
+Normal rank
@@ Property / cites work @@
+Automating program analysis
@@ Property / cites work: Automating program analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Multivariate amortized resource analysis
@@ Property / cites work: Multivariate amortized resource analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Towards automatic resource bound analysis for OCaml
+Normal rank
@@ Property / cites work @@
+Static prediction of heap space usage for first-order functional programs
+Normal rank
@@ Property / cites work @@
+A verified compiler from Isabelle/HOL to CakeML
@@ Property / cites work: A verified compiler from Isabelle/HOL to CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+Q2721966
@@ Property / cites work: Q2721966 / rank @@
+Normal rank
@@ Property / cites work @@
+The derivation of a tighter bound for top-down skew heaps
+Normal rank
@@ Property / cites work @@
+Partial Recursive Functions in Higher-Order Logic
@@ Property / cites work: Partial Recursive Functions in Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+CakeML
@@ Property / cites work: CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+Contract-based resource verification for higher-order functions with memoization
+Normal rank
@@ Property / cites work @@
+A Coq Library for Internal Verification of Running-Times
+Normal rank
@@ Property / cites work @@
+Amortized Complexity Verified
@@ Property / cites work: Amortized Complexity Verified / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Functional Correctness Proofs for Functional Search Trees
+Normal rank
@@ Property / cites work @@
+Verified Root-Balanced Trees
@@ Property / cites work: Verified Root-Balanced Trees / rank @@
+Normal rank
@@ Property / cites work @@
+Concrete Semantics
@@ Property / cites work: Concrete Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Purely Functional Data Structures
@@ Property / cites work: Purely Functional Data Structures / rank @@
+Normal rank
@@ Property / cites work @@
+Q4038672
@@ Property / cites work: Q4038672 / rank @@
+Normal rank
@@ Property / cites work @@
+A systematic analysis of splaying
@@ Property / cites work: A systematic analysis of splaying / rank @@
+Normal rank
@@ Property / cites work @@
+Self-adjusting binary search trees
@@ Property / cites work: Self-adjusting binary search trees / rank @@
+Normal rank
@@ Property / cites work @@
+Self-Adjusting Heaps
@@ Property / cites work: Self-Adjusting Heaps / rank @@
+Normal rank
@@ Property / cites work @@
+Amortized Computational Complexity
@@ Property / cites work: Amortized Computational Complexity / rank @@
+Normal rank
@@ Property / cites work @@
+Implementation of Functional Languages
@@ Property / cites work: Implementation of Functional Languages / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical program analysis
@@ Property / cites work: Mechanical program analysis / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:670702