Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                           Lundi 1 juillet, 10h30

                            --------------------
                            Daniel de Rauglaudre
                            --------------------

                                   INRIA

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

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.