English

Efficient integer arithmetic in Coq.

The Coq proof assistant has the particularity to let the user mix proofs and computations. This makes it possible to perform within Coq cerfified computations. One example of such application is the certification of large prime numbers [1]

To make this possible, it is crucial to have an efficient library for integer arithmeticc. Currently, the most efficient one is purely functional and uses complete binary trees [2]

The goal of this internship is to evaluate in which extends the imperative features recently added to the Coq system [3] could be used to provide an even more efficient library.

Français

Arithmétique entière efficace en Coq.

L'assistant de preuve Coq a la particularité de mélanger preuve et calcul. Il permet, en particulier, de faire du calcul certifié. Ceci a permis, par exemple, de certifier la primalité de grands nombres premiers [1]

Pour de telles applications, avoir une bibliothèque efficace pour faire du calcul sur les entiers est crucial. Pour l'instant, la bibliothèque la plus efficace dans Coq est purement fonctionnelle et est basée sur des arbres binaires complets [2]

L'objectif de ce stage est de voir si on ne pourrait pas utiliser les traits impératifs introduits récemment dans Coq [3] pour proposer une bibliothèque encore plus efficace.

Laurent Théry