Proofs of randomized algorithms in Coq

DOI10.1016/j.scico.2007.09.002zbMath1178.68667OpenAlexW2154231274MaRDI 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 algorithmsfunctional languageaxiomatic semanticscall-by-valuemonadic interpretationprobability framingproof of partial and total correctness

Mathematics Subject Classification ID

Randomized algorithms (68W20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms ⋮ The expectation monad in quantum foundations ⋮ Formalizing Probabilistic Noninterference ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ Model Checking Temporal Properties of Recursive Probabilistic Programs ⋮ Formal probabilistic analysis of detection properties in wireless sensor networks ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Automated reasoning for probabilistic sequential programs with theorem proving ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Verified analysis of random binary tree structures ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ Beyond Provable Security Verifiable IND-CCA Security of OAEP ⋮ Formalising Semantics for Expected Running Time of Probabilistic Programs ⋮ Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory ⋮ Real-time MLton: A Standard ML runtime for real-time functional programs ⋮ On the correctness of monadic backward induction ⋮ Formalization of Shannon's theorems

Uses Software

• Coq

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