Proofs of Randomized Algorithms in Coq

DOI10.1007/11783596_6zbMath1235.68325OpenAlexW2174515752MaRDI QIDQ3618814

Philippe Audebaud, Christine Paulin-Mohring

Publication date: 2 April 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11783596_6

Mathematics Subject Classification ID

Related Items (8)

Synthetic topology in Homotopy Type Theory for probabilistic programming ⋮ Probabilistic operational semantics for the lambda calculus ⋮ Some Domain Theory and Denotational Semantics in Coq ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ Proofs of randomized algorithms in Coq ⋮ Reasoning about conditional probabilities in a higher-order-logic theorem prover ⋮ A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq ⋮ Using theorem proving to verify expectation and variance for discrete random variables

Uses Software

• Coq

This page was built for publication: Proofs of Randomized Algorithms in Coq