Proofs of randomized algorithms in Coq

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

zbMATH Keywords

randomized algorithms; functional language; axiomatic semantics; call-by-value; monadic interpretation; probability framing; proof of partial and total correctness

Mathematics Subject Classification ID

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, 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, CryptHOL: game-based proofs in higher-order logic, Formalization of Shannon's theorems, 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

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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