Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.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

                            JEUDI 22 mars, 10h30

                             ------------------
                             Séverine Maingaud
                             ------------------

                                   IRILL

       =============================================================
       Certification de programmes impératifs en logique dynamique:
                 le cas du lambda-calcul avec références
       =============================================================

MLDL est un système formel de certification dédié à un langage de
programmation mélant fonctionnel et impératif (MLimp). L'approche
consiste à prouver l'adéquation entre un programme et sa spécification
(les deux objets étant déjà donnés). Ce système est basé sur une
logique dynamique du second ordre, adaptée à MLimp, dont le système
déductif combine des étapes de déduction purement logiques et des
étapes d'évaluation symbolique.  L'intérêt de la logique dynamique est
de pouvoir raisonner sur les états mémoire grâce à des modalités dans
le même esprit que les substitutions généralisées de la Méthode
B. Je présenterai également un modèle de MLDL qui permet d'en déduire sa
cohérence. Ce modèle combine des aspects de sémantique de Kripke (pour
modéliser la logique) et de sémantique dénotationnelle (pour modéliser
le langage de programmation).