Proofs of randomized algorithms in Coq
In: Science of Computer Programming Science of Computer Programming, 2009, ⟨10.1016/j.scico.2007.09.002⟩ Science of Computer Programming, Elsevier, 2009, ⟨10.1016/j.scico.2007.09.002⟩; (2009-06-01)
Online
unknown
Zugriff:
Randomized algorithms are widely used for finding efficiently approximated solutions to complex problems, for instance primality testing and for obtaining good average behavior. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of programs. Thus, providing tools for the mechanization of reasoning is an important issue. This 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 distributions (Giry, Ramsey and Pfeffer). It does not require the definition of an operational semantics for the language nor the development of a complex formalization of measure theory. Instead it uses functional and algebraic properties of unit interval. Using this model, we show the validity of general rules for estimating the probability for a randomized algorithm to satisfy specified properties. This approach addresses only discrete distributions and gives rules for analyzing general recursive functions.We apply this theory to the formal proof of a program implementing a Bernoulli distribution from a coin flip and to the (partial) termination of several programs. All the theories and results presented in this paper have been fully formalized and proved in the Coq proof assistant.
Titel: |
Proofs of randomized algorithms in Coq
|
---|---|
Autor/in / Beteiligte Person: | Paulin-Mohring, Christine ; Audebaud, Philippe ; Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) ; Laboratoire de Recherche en Informatique (LRI) ; Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) ; Proof of Programs (PROVAL) ; Université Paris-Sud - Paris 11 (UP11)-Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) ; ANR-07-SESU-0010,SCALP,Security of Cryptographic Algorithms with Probabilities(2007) ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-École normale supérieure - Lyon (ENS Lyon) |
Link: | |
Quelle: | Science of Computer Programming Science of Computer Programming, 2009, ⟨10.1016/j.scico.2007.09.002⟩ Science of Computer Programming, Elsevier, 2009, ⟨10.1016/j.scico.2007.09.002⟩; (2009-06-01) |
Veröffentlichung: | HAL CCSD, 2009 |
Medientyp: | unknown |
ISSN: | 0167-6423 (print) |
Schlagwort: |
|
Sonstiges: |
|