Subject: Mechanizing the proof of correction of a compiler using Type Theory
Jour: 13/10/98 (Mardi 13 octobre)

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                    Salle de confe'rence du batiment 11

                          Mardi 13 octobre, 10h30


                            -------------------
                               Yves Bertot
                            -------------------

                                  INRIA  
                         Sophia-Antipolis- projet CROAP

    ============================================================ 

          Ve'rification me'canique de la correction 
          d'un compilateur en The'orie des Types

    ============================================================


   Depuis plus de trente ans, on a de'veloppe' des programmes pour
effectuer des mathe'matiques sur ordinateur.  En particulier, certains
domaines de recherche se sont concentre's sur la repre'sentation des
e'nonce's logiques et des preuves sur l'ordinateur, la de'monstration
automatique, et la ve'rification automatique de de'monstrations donne'es
manuellement par l'utilisateur.  Un re'sultat pratique de ce domaine de 
recherche est qu'il est maintenant possible d'utiliser des ordinateurs 
pour ve'rifier formellement que des programmes respectent leur
spe'cifications.
 
   Comme e'tude de cas, nous nous sommes concentre's sur la
de'monstration qu'un compilateur respecte la signification des
programmes qu'il compile.  Le programme compile' (en langage
assembleur), effectue exactement les me^mes calculs que le programme
source.  Cette de'monstration a e'te' comple`tement formalise'e a` l'aide du 
calcul des construction inductives, une variante de la the'orie des
types bien adapte'e pour de'crire la se'mantique des deux langages de
programmation et le comportement du compilateur.

   Les contributions principales de ce travail sont trois the'ore`mes
qui permettent d'utiliser la structure du programme source pour
raisonner sur l'exe'cution du programme compile', et les techniques
ge'ne'rales qui ont e'te' utilise'es pour obtenir et ve'rifier les
de'monstrations de ces the'ore`mes.