Verified tail bounds for randomized programs

DOI10.1007/978-3-319-94821-8_33OpenAlexW2809851475MaRDI QIDQ1791202

Robert Harper, Joseph Tassarotti

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_33

Mathematics Subject Classification ID

Randomized algorithms (68W20) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (6)

Foundations for entailment checking in quantitative separation logic ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Verified analysis of random binary tree structures ⋮ Computing expected runtimes for constant probability programs ⋮ Probabilistic Analysis of Binary Sessions

Uses Software

• Coq
• Isabelle/HOL
• Coquelicot
• QuickSort Cost
• Treaps

This page was built for publication: Verified tail bounds for randomized programs