M. Aigner and G. M. Ziegler, Proofs from THE BOOK, 1998.

Y. Bertot, N. Magaud, and P. Zimmermann, A GMP program computing square roots and its proof within Coq, Journal of Automated Reasoning, 2003.

O. Caprotti and M. Oostdijk, Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles, Journal of Symbolic Computation, vol.32, issue.1-2, pp.55-70, 2001.
DOI : 10.1006/jsco.2001.0457

P. Erdös, Beweis eines Satzes von Tschebyschef, Acta Scientifica Mathematica, pp.194-198, 1932.

J. Filliâtre, Proof of Imperative Programs in Type Theory, TYPES '98, 1998.
DOI : 10.1007/3-540-48167-2_6

J. Harrison, Floating point verification in HOL, Higher Order Logic Theorem Proving and Its Applications, pp.186-199, 1995.
DOI : 10.1007/3-540-60275-5_65

J. Harrison and L. Théry, A Skeptic's Approach to Combining HOL and Maple, Journal of Automated Reasoning, vol.21, issue.3, pp.279-294, 1998.
DOI : 10.1023/A:1006023127567

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-80, 1969.
DOI : 10.1145/363235.363259

E. Donald and . Knuth, The Art of Computer Programming, : Fundamental Algorithms, pp.147-149, 1997.

. Pcoq, A Graphical User-interface to Coq

A. Slinko, Number Theory Tutorial 5: Bertrand's Postulate

I. Unité-de-recherche and . Lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38330 Montbonnot-St, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399