L'objet de ce stage sera la formalisation de cette représentation dans le système Coq. Ce travail présente un double intérêt : sur le plan théorique, il permettra de faire des formalisations constructives de résultats utilisant cette classe de réels (par exemple, le théorème de Wedderburn sur les anneaux intègres finis); sur le plan pratique, il permettra la formulation effectives de nombreux calculs: diagonalisation de matrices, construction de polynômes irréductibles, théorie de Galois, théorie algébrique des nombres... dans Coq.
Le travail aura lieu au sein de l'équipe-projet INRIA TypiCal à l'Ecole Polytechnique, en contact avec le projet Composants Mathématiques du Centre de Recherche Commun Inria - Microsoft Research à Orsay. Le travail s'appuyera d'une part sur les travaux de ce second projet sur la formalisaton de la théorie des groupes finis, et également des compétences d'Alin Bostan, spécialiste des nombres algébriques au sein de Centre Commun.
Le sujet s'intègre dans un effort beaucoup plus vaste de développement de bibliothèques calculatoires certifiées en Coq. Il prolonge directement et ré-utilise les algorithmes efficaces de manipulation de polynômes, par exemple.