article

Proofs of randomized algorithms in Coq

Authors:

Philippe Audebaud,

Christine Paulin-MohringAuthors Info & Claims

Science of Computer Programming, Volume 74, Issue 8

Pages 568 - 589

https://doi.org/10.1016/j.scico.2007.09.002

Published: 01 June 2009 Publication History

Abstract

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.

References

[1]

Audebaud, P. and Paulin-Mohring, C., Proofs of randomized algorithms in Coq. In: Uustalu, T. (Ed.), Lect. Notes in Comput. Sci., vol. 4014. Springer, Berlin. pp. 49-68.

Digital Library

[2]

M. Escardó, A. Simpson, A universal characterization of the closed euclidean interval (extended abstract), in: Proc. of 16th Ann. IEEE Symp. on Logic in Computer Science, LICS 2001 Boston, MA, June 2001, IEEE CS Press, Los Alamitos, CA, pp. 115ï¿125

Digital Library

[3]

Filliâtre, J.-C., The Why Verification Tool. 2002.

[4]

Filliâtre, J.-C., Verification of non-functional programs using interpretations in type theory. J. Funct. Programming. v13 i4. 709-745.

Digital Library

[5]

Geuvers, H. and Niqui, M., Constructive reals in Coq: Axioms and categoricity. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (Eds.), Lect. Notes in Comput. Sci., vol. 2277. Springer, Berlin. pp. 79-95.

Digital Library

[6]

Geuvers, H., Niqui, M., Spitters, B. and Wiedijk, F., Constructive analysis, types and exact real numbers. Math. Structures Comput. Sci. v17 i1. 3-36.

Digital Library

[7]

Giry, M., A categorical approach to probability theory. In: Banaschewski, B. (Ed.), Lect. Notes in Math., vol. 915. Springer, Berlin. pp. 69-85.

[8]

Hasan, O. and Tahar, S., Formalization of continuous probability distributions. In: Pfenning, F. (Ed.), Lect. Notes in Artif. Intell., vol. 4603. Springer, Berlin. pp. 3-18.

Digital Library

[9]

Hurd, J., A formal approach to probabilistic termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (Eds.), Lect. Notes in Comput. Sci., vol. 2410. Springer, Berlin. pp. 230-245.

Digital Library

[10]

J. Hurd, Formal verification of probabilistic algorithms, Ph.D. Thesis, Univ. of Cambridge, 2002

[11]

Hurd, J., Verification of the Millerï¿Rabin probabilistic primality test. J. Log. Algebr. Program. v50 i1ï¿2. 3-21.

[12]

Hurd, J., McIver, A. and Morgan, C., Probabilistic guarded commands mechanized in HOL. In: Cerone, A., Di Pierro, A. (Eds.), Electron. Notes in Theor. Comput. Sci., vol. 112. Elsevier, Amsterdam. pp. 95-111.

[13]

C. Jones, Probabilistic non-determinism, Ph.D. Thesis, Univ. of Edinburgh, 1989

Digital Library

[14]

Jones, C. and Plotkin, G., A probabilistic powerdomain of evaluations. In: Proc. of 4th Ann. IEEE Symp. on Logic in Computer Science, IEEE CS Press, Los Alamitos, CA. pp. 186-195.

Digital Library

[15]

Kozen, D., Semantics of probabilistic programs. J. Comput. System Sci. v22. 328-350.

[16]

Kozen, D., A probabilistic PDL. In: Proc. of 15th Ann. ACM Symp. on Theory of Computing, ACM Press, New York. pp. 291-297.

Digital Library

[17]

F.W. Lawvere, The category of probabilistic mappings, 1962. Preprint

[18]

McIver, A. and Morgan, C., Abstraction, refinement and proof for probabilistic systems. In: Technical Monographs in Computer Science, Springer, New York.

Digital Library

[19]

Moggi, E., Notions of computation and monads. Inform. and Comput. v93 i1. 55-92.

Digital Library

[20]

Morgan, C. and McIver, A., pGCL: Formal reasoning for random algorithms. South African Comput. J. v22. 14-27.

[21]

Park, S., Pfenning, F. and Thrun, S., A probabilistic language based upon sampling functions. In: Proc. of 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, ACM Press, New York. pp. 171-182.

Digital Library

[22]

C. Paulin-Mohring, A library for reasoning on randomized algorithms in Coq, Description of a Coq Contribution, INRIA & Univ. Paris Sud, 2007. URL http://www.lri.fr/~paulin/ALEA/library.pdf

[23]

Pfenning, F. and Davies, R., A judgmental reconstruction of modal logic. Math. Structures Comput. Sci. v11 i4. 511-540.

Digital Library

[24]

Ramsey, N. and Pfeffer, A., Stochastic lambda calculus and monads of probability distributions. In: Conf. Record of 29th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, ACM Press, New York. pp. 154-165.

Digital Library

[25]

Scott, D., Lattice theory, data types, and semantics. In: Rustin, R. (Ed.), Courant Computer Science Symposia, vol. 2. pp. 65-106.

[26]

Ycart, B., . In: Collection SMAI Mathématiques et Applications, vol. 39. Springer, Berlin.

Cited By

Feng SChen MSu HKaminski BKatoen JZhan N(2023)Lower Bounds for Possibly Divergent Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/35860517:OOPSLA1(696-726)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586051
Affeldt RCohen CSaito AKrebbers RTraytel DPientka BZdancewic S(2023)Semantics of Probabilistic Programs using s-Finite Kernels in CoqProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575691(3-16)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575691
Saito AAffeldt R(2023)Experimenting with an Intrinsically-Typed Probabilistic Programming Language in CoqProgramming Languages and Systems10.1007/978-981-99-8311-7_9(182-202)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_9
Show More Cited By

Proofs of randomized algorithms in Coq
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Proofs, tests and continuation passing style

The concept of syntactical duality is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the proof/test duality ...
Interactive Matching Logic Proofs in Coq
Theoretical Aspects of Computing – ICTAC 2023
Abstract
Matching logic (ML) is a formalism for specifying and reasoning about mathematical structures by means of patterns and pattern matching. Previously, it has been used to capture a number of other logics, e.g., separation logic with recursive ...
The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Copyright © Elsevier B.V. © 2009.

Publisher

Elsevier North-Holland, Inc.

United States

Publication History

Published: 01 June 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Feng SChen MSu HKaminski BKatoen JZhan N(2023)Lower Bounds for Possibly Divergent Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/35860517:OOPSLA1(696-726)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586051
Affeldt RCohen CSaito AKrebbers RTraytel DPientka BZdancewic S(2023)Semantics of Probabilistic Programs using s-Finite Kernels in CoqProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575691(3-16)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575691
Saito AAffeldt R(2023)Experimenting with an Intrinsically-Typed Probabilistic Programming Language in CoqProgramming Languages and Systems10.1007/978-981-99-8311-7_9(182-202)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_9
Lochbihler A(2022)A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability TheoryJournal of Automated Reasoning10.1007/s10817-022-09616-466:4(585-610)Online publication date: 1-Nov-2022
https://dl.acm.org/doi/10.1007/s10817-022-09616-4
Ye KFoster SWoodcock J(2021)Automated Reasoning for Probabilistic Sequential Programs with Theorem ProvingRelational and Algebraic Methods in Computer Science10.1007/978-3-030-88701-8_28(465-482)Online publication date: 2-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-88701-8_28
Eberl MHaslbeck MNipkow T(2020)Verified Analysis of Random Binary Tree StructuresJournal of Automated Reasoning10.1007/s10817-020-09545-064:5(879-910)Online publication date: 1-Jun-2020
https://dl.acm.org/doi/10.1007/s10817-020-09545-0
Nipkow TEberl MHaslbeck M(2020)Verified Textbook AlgorithmsAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_2(25-53)Online publication date: 19-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-59152-6_2
Gopinathan KSergey I(2020)Certifying Certainty and Uncertainty in Approximate Membership Query StructuresComputer Aided Verification10.1007/978-3-030-53291-8_16(279-303)Online publication date: 21-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-53291-8_16
Shivkumar BMurphy JZiarek L(2020)RTMLton: An SML Runtime for Real-Time SystemsPractical Aspects of Declarative Languages10.1007/978-3-030-39197-3_8(113-130)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1007/978-3-030-39197-3_8
Hark MKaminski BGiesl JKatoen J(2019)Aiming low is harder: induction for lower bounds in probabilistic program verificationProceedings of the ACM on Programming Languages10.1145/33711054:POPL(1-28)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371105
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents