Proofs of randomized algorithms in Coq
From MaRDI portal
Publication:923886
DOI10.1016/j.scico.2007.09.002zbMath1178.68667MaRDI QIDQ923886
Philippe Audebaud, Christine Paulin-Mohring
Publication date: 24 July 2009
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00431771/file/postprint.pdf
randomized algorithms; functional language; axiomatic semantics; call-by-value; monadic interpretation; probability framing; proof of partial and total correctness
68W20: Randomized algorithms
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Real-time MLton: A Standard ML runtime for real-time functional programs, On the correctness of monadic backward induction, Verified analysis of random binary tree structures, VPHL: a verified partial-correctness logic for probabilistic programs, Model Checking Temporal Properties of Recursive Probabilistic Programs, The expectation monad in quantum foundations, Formal probabilistic analysis of detection properties in wireless sensor networks, Markov chains and Markov decision processes in Isabelle/HOL, A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory, CryptHOL: game-based proofs in higher-order logic, Formalization of Shannon's theorems, Automated reasoning for probabilistic sequential programs with theorem proving, Probabilistic Functions and Cryptographic Oracles in Higher Order Logic, Formalising Semantics for Expected Running Time of Probabilistic Programs, Formalizing Probabilistic Noninterference, A Formalized Hierarchy of Probabilistic System Types, Beyond Provable Security Verifiable IND-CCA Security of OAEP, Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience, Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms
Uses Software
Cites Work
- Markovian models and algorithms
- Notions of computation and monads
- Semantics of probabilistic programs
- Verification of the Miller-Rabin probabilistic primality test.
- Probabilistic guarded commands mechanized in HOL
- A judgmental reconstruction of modal logic
- Constructive analysis, types and exact real numbers
- Formalization of Continuous Probability Distributions
- Proofs of Randomized Algorithms in Coq
- Verification of non-functional programs using interpretations in type theory
- Abstraction, Refinement and Proof for Probabilistic Systems
- Stochastic lambda calculus and monads of probability distributions
- A probabilistic language based upon sampling functions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item