To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 09/02/07 - 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 9 fevrier, 10h30

                               --------------
                               Julien Narboux
                               --------------

                                 TU München

          =======================================================
          Quelques preuves typiques dans les langages avec lieurs
                      en utilisant l'approche nominale
          =======================================================

Le package Nominal est une extension de Isabelle/HOL dont le but est de
faciliter le développement de preuves formelles dans le contexte des
langages avec lieurs.

Après une introduction au package Nominal, je presenterai deux
développements Isabelle/HOL. Le premier, inspiré par un challenge
suggéré par A. Chlipala sur la mailing liste PoplMark,  consiste en une
preuve de normalisation pour une extension du lambda calcul avec types
sommes et produits en se basant sur une sémantique à grands pas. Le
deuxième est une formalisation du chapitre "Logical Relations and a Case
Study in Equivalence" de Crary du livre "Advanced Topics in Types and
Programming Languages".

L'originalité de l'approche réside dans le fait que nous nous attachons
à produire des preuves lisibles qui ressemblent le plus possible aux
preuves traditionnelles. Pour cela, nous prouvons
des principes d'induction, des lemmes d'inversion et utilisons des
tactiques adaptées à la preuve formelle dans un langage avec lieurs. Je
presenterai ces différents outils.