Sites Inria

Séminaire des équipes de recherche

Théorème de Puiseux en OCaml et en Coq

  • Date : 1/07/2013
  • Lieu : Rocquencourt, Amphithéâtre A. Turing - bâtiment 1
  • Intervenant(s) : Daniel de Rauglaudre
  • Organisateur(s) : Gallium

Le théorème de Puiseux affirme que tout polynôme à coefficients en séries de Puiseux (à puissances rationnelles) admet une racine.
La démonstration classique par Robert Walker du théorème est réputée constructive : un algorithme mathématique permet de calculer par induction les coefficients et les puissances de chaque série  solution. On exposera l'implémentation de cet algorithme en OCaml, ainsi que la traduction du théorème en Coq, en vue d'en établir une preuve formelle. Le parallèle entre OCaml et Coq est facilité par une extension de syntaxe Camlp5, permettant d'écrire de la syntaxe Coq dans le code OCaml. Il s'agit d'un travail en cours de développement.
La partie OCaml est interfacée avec MPFR, bibliothèque d'arithmétique flottante en précision arbitraire.

Mots-clés : Gallium Séminaire Paris - Rocquencourt

Haut de page

Suivez Inria