... scientifique¹

Il faut prendre ici l'expression ``calcul scientifique'' dans son sens le plus large, qui inclut calcul numérique et calcul formel, et qu'on pourrait remplacer par calcul mathématique.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Maple²

Depuis, et en partie à cause de cette expérience, Maple a amélioré son implantation de l'algorithme de Buchberger.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... calculs).³

Nous ne négligerons pas cet aspect pédagogique et essaierons de confronter nos réalisations au monde universitaire : après tout, ce sont les ingénieurs de demain qui y sont formés.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... ensembles⁴

Voir la librairie SETS de Coq par Gilles Kahn et Gérard Huet.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... catégories⁵

Voir la librairie ALGEBRA d'Amokrane Saïbi, disponible dans la prochaine version de Coq.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... algébrique⁶

C'est le sujet de la thèse, financée par une bourse centre de l'INRIA Sophia Antipolis, que commence Laurent Chicli, co-dirigée par André Hirschowitz et Loïc Pottier.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... fondé⁷

C'est le sujet de thèse d'Antonia Balaa, dirigée par Yves Bertot.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Figue⁸

Figue est en fait issu d'une collaboration initiale avec Laurent Hascoët.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... l'arithmétique⁹

Indépendamment de l'attrait que peut avoir ce travail

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... Buchberger.¹⁰

Un autre enseignement de ce travail est que prouver formellement un algorithme en implique une compréhension profonde, ce qui peut conduire à le simplifier et à l'améliorer, comme cela a été le cas ici : l'algorithme de calcul de bases de Gröbner qu'a prouvé Laurent Théry est original et diffère de celui dont il s'est inspiré [23], même s'il en reste très proche. Ceci a aussi été le cas pour l'algorithme de Cantor-Zassenhaus qu'a prouvé François Maurel.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... implémenté¹¹

http ://umpa.ens-lyon.fr/~tmignon/progra.html

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... finis¹²

Les groupes ont été abordés en Coq entre autres par Gilles Kahn (groupes finis), Yves Bertot (permutations), Laurence Rideau et Loïc Pottier (modélisation constructive/classique).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.