The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

  Aux membres du club Coq :

  Laurent Théry fera son exposé sur la formalisation du cryptage RSA
  en Coq, PVS et HOL le vendredi 26 juin^H^H^H^Hmai

----------------------------------------------------------------------
           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E

   ____              ____    .                   
  /   _   _        /    ___   __  /_  _   /     /| /|  _   __ __ _       _ 
 /   / \ / \  _   /    /   / /_  /   __| /  _  / |/ | / \ /_ /  / \ | / __|
|___ |_/ |_/     |___ /   / __/ |_  |_/ |_    /     | |_/__/ |_ |_/ |/ |_/
          /                                                                 
         /                                                                  
                          I N R I A - Rocquencourt, 
                       Salle de conférence du Bât 11

                           Vendredi 26 mai, 10h30

                               -------------
                               Laurent Théry
                               -------------

                           INRIA Sophia-Antipolis

         ==========================================================
         Une comparaison de Coq, Hol,Pvs: une preuve élémentaire de
                       l'algorithme à clé public RSA
         ==========================================================

Dans cet exposé, nous présentons une preuve élémentaire de
l'algorithme RSA qui a été réalisée dans 3 démonstrateurs différents:
Coq, HOL et PVS. Après une rapide présentation de la preuve,
nous montrerons comment les spécificités des différents 
démonstrateurs ont influé sur la preuve.