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

                             -----------------
                             Mathieu Boespflug
                             -----------------

                                    LIX

         =========================================================
         Europa, un vérificateur de types pour le lambda-pi modulo
         =========================================================

Le lambda-pi-calcul est un calcul avec types dépendants permettant
l'expression de preuves en logique minimales des prédicats. En
étendant ce calcul avec des règles de réécriture, il devient possible
d'exprimer des preuves dans des théories bien plus riches. On obtient
ainsi le lambda-pi-calcul-modulo. Un encodage de tous les PTS
fonctionnels est par exemple possible.

Se pose alors la question des stratégies à mettre en oeuvre pour
l'implantation de vérificateurs efficaces de preuves encodées ainsi.
En effet, vérifier la plus simple de ces preuves nécessite
l'application de nombreuses règles de réécriture, ce qui peut être
coûteux en temps de calcul. Je montrerai comment se tirer d'affaire à
peu de frais, en compilant les preuves exprimées dans le
lambda-pi-calcul-modulo vers un programme fonctionnel, dont
l'évaluation par des environnements d'exécution usuels en permet la
vérification. Nous ferons la démonstration de l'outil clé d'un tel
modèle, le méta-vérificateur Europa (nom encore tout à fait
temporaire), traitant de bout en bout son implantation très simple.