To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 08/06/09 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.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 8 juin, 10h30

                       ------------------------------
                       Thomas Braibant et Damien Pous
                       ------------------------------

                                   INRIA

                           ======================
                           Kleene et Kozen en Coq
                           ======================

Formaliser des choses dans un assistant de preuve s'avère souvent
pénible, de nombreuses étapes de raisonnement devant être explicitées
alors qu'elles sont d'habitude laissées au relecteur scrupuleux.  Ceci
est en particulier vrai lorsque l'on doit travailler sur des relations
binaires (réécriture, réductions, équivalences, etc...), très
intuitives, mais pas complètement triviales.

Lorsque c'est possible, une première astuce consiste à considérer les
relations de façon algébrique : en montant le niveau d'abstraction, on
facilite la formalisation de certaines preuves. Une fois ce pas
franchi, on réalise que les relations binaires sont un modèle des
algèbres de Kleene, décidables par la théorie des automates finis.

Nous exposerons un travail en cours, sur une formalisation Coq des
automates - via des matrices, afin d'obtenir une tactique de décision
des algèbres de Kleene, par réflection. Plus généralement, nous
exposerons les outils que nous développons pour raisonner sur ce genre
de structures algébriques.