A Coq Library for Internal Verification of Running-Times

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

Mathematics Subject Classification ID

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

• Coq
• OCaml
• SPEED

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