A formalization of Knuth's algorithm and Bertrand's postulate.

It is composed of :

- A proof of correctness of the algorithm for computing the first n prime numbers as described in `The Art of Computer Programming'.

- A proof of Bertrand's postulate that there is always a prime number between n and 2n for n greater than 2.

A formalization of Buchberger's algorithm.

It is composed of :

- A proof of correctness of the algorithm as described in `A machine checked implementation of Buchberger's algorithm' in JAR Jan. 2001.

- An implementation of the algorithm. With respect to the paper, terms are not abstracted but built directly from coef and monomials.

- A constructive proof of Dickson's lemma due to Henrik Persson

A formalization of Huffman algorithm.

It is composed of :

- A proof of correctness of the algorithm as described in `A Method for the Construction of Minimum-Redundancy Codes'.

- An extracted version of the algorithm that can be executed under ocaml

A library for floating point numbers. It is described in

`A generic library of floating-point number and its application to exact computing' in TPHOLs 2001.

A standard result of number theory:

- A number n can be written as the sum of two square numbers if and only if each prime factor p of n that is equal to 3 modulo 4 has its exponent in the decomposition of n that is even.

A direct transcription in Coq of the paper:

Uber die Vollstandingen einer gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.

Comptes Rendus du premier Congrès des Mathématiciens des Pays slaves, Warszawa, 1929.

A translation in English is available at http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR84-639

R. Stansifer, Presburger's Article on Integer Arithmetic: Remarks and Translation, Technical Report TR 84-639, Cornell.

A proof of correctness of RSA algorithm that relies on Fermat's little theorem

A formalization of Stalmarck's algorithm. It is composed of :

- a proof of correctness of the algorithm as described in `A formalization of Stalmarck's algorithm in COQ' TPHOLs2000.

- an implementation of the algorithm. With respect to the paper, this implementation is completely functional and can be used inside Coq.

- a reflected tactic Stalt, that uses the extracted code to compute an execution trace, the trace checker is then called inside Coq.

Laurent Théry Last modified: Wed Jan 5 19:41:53 MET 2005