A Coq Library for Internal Verification of Running-Times
From MaRDI portal
Publication:2798271
DOI10.1007/978-3-319-29604-3_10zbMath1475.68457OpenAlexW2408675243MaRDI QIDQ2798271
Daniel Feltey, Robert Bruce Findler, Burke Fetscher, Max New, Jay McCarthy
Publication date: 4 April 2016
Published in: Functional and Logic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-29604-3_10
Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (5)
Verified Root-Balanced Trees ⋮ Denotational semantics as a foundation for cost recurrence extraction for functional languages ⋮ Unnamed Item ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Amortized complexity verified
Uses Software
Cites Work
- Unnamed Item
- Automatic Static Cost Analysis for Parallel Programs
- Recursion and dynamic data-structures in bounded space
- 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
- A Hoare Logic for the State Monad
- Lightweight semiformal time complexity analysis for purely functional data structures
- Monads Need Not Be Endofunctors
- Subset Coercions in Coq
- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
- Parameterised notions of computation
- Three algorithms on Braun trees
- Program verification through characteristic formulae
- Resource bound certification
- SPEED
- Programming Languages and Systems
This page was built for publication: A Coq Library for Internal Verification of Running-Times