To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 03/11/08 - 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 3 novembre, 10h30

                              ---------------
                              Matthieu Sozeau
                              ---------------

                     Université Paris Sud, CNRS, INRIA

                    ===================================
                    Classes de types de première classe
                    ===================================

Les classes de types ont démontré leur utilité pour la programmation
polymorphique de haut-niveau en Haskell et la construction de
hiérarchies de structures mathématiques dans l'assistant de preuve
Isabelle. Ce mécanisme de surcharge très versatile peut se généraliser
aux types dépendants et offre alors de nouvelles formes de généricité.
Il permet aussi d'intégrer une forme de programmation logique au moment
du typage.  On présentera une implémentation légère d'un système de
classes de types de première classe dans Coq, basée sur un
enrichissement de constructions existantes du langage Gallina. On
illustrera ce nouvel outil par des exemples mettant en oeuvre les
classes pour programmer, prouver et organiser les développements en Coq.