To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 11/05/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 11 mai, 10h30

                             ------------------
                             Arthur Charguéraud
                             ------------------

                                   INRIA

       ==============================================================
       Tutoriel : Vérification Interactive de Programmes Fonctionnels
       ==============================================================

En décrivant dans Coq la syntaxe et la sémantique du noyau
purement fonctionnel de Caml, il est possible de spécifier
formellement et de vérifier interactivement des programmes
Caml purs. J'ai développé un outil implémentant cette approche,
et je l'ai utilisé en particulier pour vérifier la bibliothèque
des listes de Caml, ainsi que l'implémentation d'un compilateur-
interpréteur bytecode pour mini-ML. L'objectif de ce séminaire
est de vous apprendre à utiliser cet outil, afin que vous puissiez
vérifier vous-mêmes des programmes purement fonctionnels.

Le séminaire débutera par une introduction d'une quinzaine de
minutes aux ingrédients théoriques utilisés. Le reste du séminaire
sera consacré à la spécification et la vérification d'une série
de petits programmes par les participants. Noter que la majeure
partie du tutoriel sera organisée de sorte à pouvoir être suivie
par les personnes qui ne maîtrisent pas Coq.

Important : pour profiter pleinement de ce tutoriel, il faut
disposer d'une version de Coq v8.2 en état de marche (toutes les
releases devraient fonctionner, normalement), avec CoqIDE ou bien
Proof-General (si vous maîtrisez ce dernier). Pour tester votre
installation, vous pouvez essayer de compiler (en tapant "make")
l'archive qui se trouve sur :
http://arthur.chargueraud.org/research/2009/deep/src/distrib.tar.gz
puis de jouer interactivement le fichier "VerifMerge_proof.v".
N'hésitez pas à me contacter si vous avez besoin d'aide :
   arthur.chargueraud[at]inria.fr