The Coq mailing list

[Sandrine Blazy <sandrine.blazy AT ensiie.fr>]

                   Appel a participation

         JOURNEES FRANCOPHONES DES LANGAGES APPLICATIFS

                              INRIA

                       26 au 29 janvier 2008

                        Etretat, France

                  http://jfla.inria.fr/2008

Le programme des 19èmes JFLA est maintenant établi; vous trouverez
auprès du site des journées http://jfla.inria.fr/2008 tout
renseignement nécessaire à votre inscription.

Sandrine Blazy

************************************************************************ 
********
26 janvier 2008
---------------------
    * 15h - 15h30 Accueil - Présentation
    * 15h30 - 17h Cours Coq par Yves Bertot: Sémantiques en Coq
    * 17h - 17h30 Pause-café
    * 17h30 - 19h Cours Focal par Renaud Rioboo:
        Concevoir et organiser une librairie de mathématiques  
effectives
    * 19h00 Dîner

27 janvier 2008
---------------------
   * 9h - 10h30 Cours Coq par Yves Bertot: Sémantiques en Coq
    * 10h30 - 11h Pause-café
    * 11h30 - 12h30 Cours Focal par Renaud Rioboo:
        Concevoir et organiser une librairie de mathématiques  
effectives
    * 12h30 - 14h Déjeuner
    * 14h00 - 18h Excursion: une balade à pied
    * 19h00 Dîner

28 janvier 2008
---------------------
    * 9h00 - 10h00 Conférence invitée.
      Les types à relations.
      Pierre Weis (INRIA).
    * 10h - 10h30 Pause-café
    * 10h30 - 11h Formalisation des mathématiques: une preuve du  
théorème de Cayley-Hamilton.
      Sidi Ould Biha.
    * 11h - 11h30 A formal verification for Kantorovitch's theorem.
      Ilona Pasca.
    * 11h30 - 12h00 Vérification formelle d'un algorithme  
d'allocation de registres par coloration de graphes.
      Sandrine Blazy, Benoît Robillard et Éric Soutif.
    * 12h00 - 14h Déjeuner
    * 14h00 - 14h30 De la webradio lambda à la lambda-webradio.
      David Baelde et Samuel Mirman.
    * 14h30 - 15h Le caractère ' à la rescousse.
      Boris Yakobowski.
    * 15h00 - 15h30 Types simples, logique et coercions implicites.
      Cody Roux.
    * 15h30 - 16h Pause café
    * 16h - 16h30 SAT-Micro : petit mais costaud !.
      Sylvain Conchon, Johannes Kanig et Stéphane Lescuyer.
    * 16h30 - 17h Vérification formelle du tri par tas - Étude  
opérationnelle.
      Pascal Manoury.
    * 17h - 17h30 Métaprogrammation fonctionnelle appliquée à la  
génération d'un DSL dédié
         à la programmation parallèle.
       Julien Sérot et Joël Falcou.
    * 19h00 Dîner

29 janvier 2008
---------------------
    * 9h00 - 10h00 Conférence invitée.
      Implémentations sûres de sessions typées.
      Cédric Fournet (Microsoft Research).
    * 10h - 10h30 Pause-café
    * 10h30 - 11h00 Une axiomatique de la géométrie plane en Coq.
      Jean Duprat.
    * 11h00 - 11h30 Gagner en passant à la corde.
      Jean-Christophe Filliâtre.
    * 11h30 - 11h45 Bilan et clôture des Journées
    * 11h45 - 12h30 Déjeuner

Pour tout renseignement, contacter

    Gaëlle Dorkeld
    INRIA Rocquencourt
    Bureau des Cours et Colloques (JFLA2008)
    Domaine de Voluceau - BP 105
    78153 Le Chesnay Cedex
    Tél.: +33 (0) 1 39 63 56 00 - Fax : +33 (0) 1 39 63 56 38
    email : 
Gaelle.Dorkeld AT inria.fr
    http://jfla.inria.fr/2008/