Proofs from THE BOOK, 1998. ,
A GMP program computing square roots and its proof within Coq, Journal of Automated Reasoning, 2003. ,
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
Beweis eines Satzes von Tschebyschef, Acta Scientifica Mathematica, pp.194-198, 1932. ,
Proof of Imperative Programs in Type Theory, TYPES '98, 1998. ,
DOI : 10.1007/3-540-48167-2_6
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
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
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-80, 1969. ,
DOI : 10.1145/363235.363259
The Art of Computer Programming, : Fundamental Algorithms, pp.147-149, 1997. ,
A Graphical User-interface to Coq ,
Number Theory Tutorial 5: Bertrand's Postulate ,
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 ,
BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399 ,