P. Audebaud and C. Paulin-mohring, Proofs of Randomized Algorithms in Coq, Mathematics of Program Construction, pp.49-68, 2006.
DOI : 10.1007/11783596_6
URL : https://hal.archives-ouvertes.fr/inria-00431771

M. Escardo and A. Simpson, A universal characterization of the closed euclidean interval (extended abstract), IEEE Symp. on Logic in Computer Science, pp.115-125, 2001.

J. Filliâtre, The Why verification tool, 2002.

J. Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of functional Programming, vol.13, issue.4, pp.709-745, 2003.
DOI : 10.1017/S095679680200446X

H. Geuvers and M. Niqui, Constructive Reals in Coq: Axioms and Categoricity, Types for Proofs and Programs. Selected Papers, pp.79-95, 2002.
DOI : 10.1007/3-540-45842-5_6

H. Geuvers, M. Niqui, B. Spitters, and F. Wiedijk, Constructive analysis, types and exact real numbers, Mathematical Structures in Computer Science, vol.17, issue.01, pp.3-36, 2007.
DOI : 10.1017/S0960129506005834

M. Giry, A categorical approach to probability theory Categorical Aspects of Topology and Analysis, Lecture Notes in Mathematics, vol.915, pp.69-85, 1982.

O. Hasan and S. Tahar, Formalization of Continuous Probability Distributions, Proc. 21st Conference on Automated Deduction (CADE-21, pp.3-16, 2007.
DOI : 10.1007/978-3-540-73595-3_2

J. Hurd, A Formal Approach to Probabilistic Termination, Theorem Proving in Higher Order Logics, pp.230-245, 2002.
DOI : 10.1007/3-540-45685-6_16

J. Hurd, Formal verification of probabilistic algorithms, 2002.

J. Hurd, Verification of the Miller???Rabin probabilistic primality test, special issue on Probabilistic Techniques for the Design and Analysis of Systems, pp.3-21, 2003.
DOI : 10.1016/S1567-8326(02)00065-6

J. Hurd, A. Mciver, and C. Morgan, Probabilistic guarded commands mechanized in HOL, Quantitative Aspects of Programming Languages. ENTCS, vol.112, pp.95-111, 2005.

C. Jones, Probabilistic non-determinism, 1989.

C. Jones and G. Plotkin, A probabilistic powerdomain of evaluations, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.186-195, 1989.
DOI : 10.1109/LICS.1989.39173

D. Kozen, Semantics of probabilistic programs, 20th Annual Symposium on Foundations of Computer Science (sfcs 1979), pp.328-350, 1981.
DOI : 10.1109/SFCS.1979.38

D. Kozen, A probabilistic PDL, Proceedings of the fifteenth annual ACM symposium on Theory of computing , STOC '83, pp.291-297, 1983.
DOI : 10.1145/800061.808758

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

A. Mciver and C. Morgan, Abstraction, Refinement and Proof for Probabilistic Systems, Monographs in Computer Science, 2005.

E. Moggi, Notions of computation and monads, Information and Computation, vol.93, issue.1, pp.55-92, 1991.
DOI : 10.1016/0890-5401(91)90052-4

C. Morgan and A. Mciver, pGCL: formal reasoning for random algorithms, South African Computer Journal, vol.22, pp.14-27, 1999.

S. Park, F. Pfenning, and S. Thrun, A probabilistic language based upon sampling functions, In: ACM Symp. on Principles of Programming Languages, pp.171-182, 2005.
DOI : 10.1145/1047659.1040320
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.119.1194

C. F. Paulin-mohring and R. Davies, A library for reasoning on randomized algorithms in Coq Description of a Coq contribution A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, vol.11, issue.4, pp.511-540, 2001.

N. Ramsey and A. Pfeffer, Stochastic lambda calculus and monads of probability distributions, ACM Symp. on Principles of Programming Languages, pp.154-165, 2002.

D. Scott, Lattice theory, data types, and semantics, Formal Semantics of Programming Languages of Courant Computer Science Symposia, pp.65-106, 1972.

B. Ycart, Modèles et algorithmes markoviens, 39 in Collection SMAI Mathematiques et Applications, 2002.