Pages that link to "Item:Q923886"
From MaRDI portal
The following pages link to Proofs of randomized algorithms in Coq (Q923886):
Displaying 26 items.
- The expectation monad in quantum foundations (Q320204) (← links)
- Formal probabilistic analysis of detection properties in wireless sensor networks (Q903510) (← links)
- Markov chains and Markov decision processes in Isabelle/HOL (Q1701041) (← links)
- Verified tail bounds for randomized programs (Q1791202) (← links)
- Randomized proofs in arithmetic (Q1807460) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
- CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
- Formalization of Shannon's theorems (Q2352494) (← links)
- Automated reasoning for probabilistic sequential programs with theorem proving (Q2695373) (← links)
- (Q2754056) (← links)
- Probabilistic Functions and Cryptographic Oracles in Higher Order Logic (Q2802495) (← links)
- Formalising Semantics for Expected Running Time of Probabilistic Programs (Q2829281) (← links)
- Formalizing Probabilistic Noninterference (Q2938053) (← links)
- A Formalized Hierarchy of Probabilistic System Types (Q2945633) (← links)
- Beyond Provable Security Verifiable IND-CCA Security of OAEP (Q3073706) (← links)
- Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience (Q3100218) (← links)
- Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms (Q3179391) (← links)
- A Randomized Algorithm for BBCSPs in the Prover-Verifier Model (Q3525105) (← links)
- Proofs of Randomized Algorithms in Coq (Q3618814) (← links)
- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq (Q3638257) (← links)
- Real-time MLton: A Standard ML runtime for real-time functional programs (Q5019014) (← links)
- On the correctness of monadic backward induction (Q5019023) (← links)
- Verified analysis of random binary tree structures (Q5919010) (← links)
- VPHL: a verified partial-correctness logic for probabilistic programs (Q5971408) (← links)
- Model Checking Temporal Properties of Recursive Probabilistic Programs (Q6137848) (← links)
- Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving (Q6639734) (← links)
