The Coq mailing list

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

[English below]

L'équipe Coq est heureuse de vous informer de la tenue d'une 2ème
journée thématique le mardi 14 mars 2000 à l'INRIA Rocquencourt.

Des utilisateurs ayant testé la formalisation d'un même développement
simultanément dans plusieurs systèmes d'aide à la preuve viendront
faire part de leur expérience.

  Le programme actuellement prévu est le suivant :

  Tristan Crolard (LACL - Université de Créteil)
     Formalisation et vérification du problème du "passage à niveau"
     dans Coq et PVS.

  Laurent Théry (INRIA Sophia)
     Une comparaison de Coq, Hol, Pvs : une preuve élémentaire de
     l'algorithme à clé public RSA

  Jean-Paul Bodeveix (IRIT - Université de Toulouse)
     Formalisation de la méthode B en Coq et PVS
     Travail commun avec Mamoun Filali et César Muñoz

  Pierre Casteran (LABRI - Université de Bordeaux)
     Preuves sur les systèmes de transitions en Isabelle/HOL et
     partiellement en Coq (travail commun avec Davy Rouillard)

  La journée commencera à 11h et se terminera vers 17h30.

  Une version actualisée du programme avec les résumés est disponible
à l'adresse "http://coq.inria.fr/seminaires/comparaison" ;.

----------------------------------------------------------------------
[English version]

  A thematic day on the comparison of a same formalisation in various
proof assistants will hold on Tuesday, 14th march 2000, at INRIA
Rocquencourt, near Paris.

  Preliminary program includes the following talks

  Tristan Crolard (LACL - University of Créteil)
     Formalisation and verification of "level crossing" problem in Coq and PVS

  Laurent Théry (INRIA Sophia)
     Comparing Coq, HOL, PVS  on a simple proof of the RSA Public
     Key Encryption Algorithm.

  Jean-Paul Bodeveix (IRIT - University of Toulouse)
     Formalisation of the B-method in Coq and PVS
     Joint work with Mamoun Filali and César Muñoz

  Pierre Casteran (LABRI - University of Bordeaux)
     Proofs on transition systems in Isabelle/HOL and partially Coq
     (joint work with Davy Rouillard)

  Talks will start at 11 am and end around 5.30 pm. Updated program and
abstracts can be found at "http://coq.inria.fr/seminaires/comparaison";.
Please send a mail to 
Hugo.Herbelin AT inria.fr
 in case you plan to come.