Proofs of Randomized Algorithms in Coq
From MaRDI portal
Recommendations
- Proofs of randomized algorithms in Coq
- Certified impossibility results and analyses in Coq of some randomised distributed algorithms
- Coarse reducibility and algorithmic randomness
- Coalgebraic tools for randomness-conserving protocols
- Coalgebraic tools for randomness-conserving protocols
- Randomized proofs in arithmetic
- Computer Aided Verification
- Proof by computation in the Coq system
- scientific article; zbMATH DE number 1670755
Cited in
(14)- Synthetic topology in Homotopy Type Theory for probabilistic programming
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- Some Domain Theory and Denotational Semantics in Coq
- A Randomized Algorithm for BBCSPs in the Prover-Verifier Model
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- Verified tail bounds for randomized programs
- Proofs of randomized algorithms in Coq
- scientific article; zbMATH DE number 1670755 (Why is no real title available?)
- 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
- Probabilistic operational semantics for the lambda calculus
- Randomized proofs in arithmetic
- Certified impossibility results and analyses in Coq of some randomised distributed algorithms
- RDA: a Coq library to reason about randomised distributed algorithms in the message passing model
This page was built for publication: Proofs of Randomized Algorithms in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3618814)
