Proofs of Randomized Algorithms in Coq Export

@incollection{citeulike:4238182, abstract = {Randomized algorithms are widely used either for finding efficiently approximated solutions to complex problems, for instance primality testing, or for obtaining good average behavior, for instance in distributed computing. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of the programs. Providing tools for the mechanization of reasoning is consequently an important issue. Our paper presents a new method for proving properties of randomized algorithms in a proof assistant based on higher-order logic. It is based on the monadic interpretation of randomized programs as probabilistic distribution [1]. It does not require the definition of an operational semantics for the language nor the development of a complex formalization of measure theory, but only use functionals and algebraic properties of the unit interval. Using this model, we show the validity of general rules for estimating the probability for a randomized algorithm to satisfy certain properties, in particular in the case of general recursive functions.}, author = {Audebaud, Philippe and Paulin-Mohring, Christine}, citeulike-article-id = {4238182}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/11783596_6}, citeulike-linkout-1 = {http://www.springerlink.com/content/m685t3n66456g38k}, doi = {10.1007/11783596_6}, journal = {Mathematics of Program Construction}, keywords = {coq, formal-proof, project-p2p-theory, proof, randomized-algorithm}, pages = {49--68}, posted-at = {2009-04-21 08:09:54}, priority = {0}, title = {Proofs of Randomized Algorithms in Coq}, url = {http://dx.doi.org/10.1007/11783596_6}, year = {2006} }

TY - CHAP ID - citeulike:4238182 L3 - citeulike-article-id:4238182 N2 - Randomized algorithms are widely used either for finding efficiently approximated solutions to complex problems, for instance primality testing, or for obtaining good average behavior, for instance in distributed computing. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of the programs. Providing tools for the mechanization of reasoning is consequently an important issue. Our paper presents a new method for proving properties of randomized algorithms in a proof assistant based on higher-order logic. It is based on the monadic interpretation of randomized programs as probabilistic distribution [1]. It does not require the definition of an operational semantics for the language nor the development of a complex formalization of measure theory, but only use functionals and algebraic properties of the unit interval. Using this model, we show the validity of general rules for estimating the probability for a randomized algorithm to satisfy certain properties, in particular in the case of general recursive functions. JF - Mathematics of Program Construction EP - 68 TI - Proofs of Randomized Algorithms in Coq SP - 49 KW - coq KW - formal-proof KW - project-p2p-theory KW - proof KW - randomized-algorithm AU - Audebaud, Philippe AU - Paulin-Mohring, Christine PY - 2006/// UR - http://dx.doi.org/10.1007/11783596_6 ER -