To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 28/04/06 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                          Vendredi 28 avril, 10h30

                              ---------------
                              Julien Signoles
                              ---------------

                                    LRI

      ===============================================================
      Obligations de preuve pour une extension de ML avec raffinement
      ===============================================================

Nous proposons une extension conservative de ML permettant de spécifier et
de vérifier des programmes de ce langage. Après avoir présenté la syntaxe
et la sémantique de cette extension, nous nous concentrerons sur
l'étude de son système de types qui garantit statiquement la correction
des expressions vis-à-vis de leurs spécifications.

Un tel système est indécidable et, pour surmonter cette difficulté, le
système de types engendre des obligations de preuve à vérifier à l'aide
d'un outil externe. Pour ce faire, il repose sur une caractérisation
logique, que nous introduirons, permettant de transformer une expression
du langage en une formule du calcul des prédicats (du second ordre). En
outre, nous expliquerons un algorithme utilisé par le système, fondé sur
des manipulations symboliques d'expressions et calculant le domaine d'une
fonction, domaine qui peut être une expression arbitrairement complexe
dans l'extension considérée.