Formalisations in Coq

Knuth's algorithm and Bertrand's postulate

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.

It includes Fermat Little Theorem and Wilson Theorem.

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.

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.

Last modified: Wed Jan 5 19:41:53 MET 2005