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.


Buchberger's algorithm


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


Huffman algorithm


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


Floating-Point Numbers


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.


Numbers equal to the sum of two square numbers


A standard result of number theory: It includes Fermat Little Theorem and Wilson Theorem.

Presburger's algorithm


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.


Rsa algorithm


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

Stalmarck's algorithm


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