To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 14/05/07 - 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 14 mai, 10h30

                               --------------
                               Bruno Bernardo
                               --------------

                                   INRIA

                ===========================================
                        Certification de Programmes
                avec le Calcul des Constructions Implicites
                ===========================================

Programmer dans le Calcul des Constructions peut se révéler pénible puisque
les programmes contiennent des informations statiques (preuves d'objets,
dépendances, décorations de types) qui ne sont pas nécessaires lors de
l'exécution.  Alexandre Miquel a défini un Calcul des Constructions Implicite
à la Curry (ICC) où les termes statiques n'apparaissent pas. Ce calcul ne
possède cependant pas la décidabilité du typage.

Dans cet exposé nous introduisons ICC*, une variante de ICC avec des termes
annotés, dont le typage est décidable.  Les types de données et les
spécifications de programmes sont enrichies par des assertions logiques
(préconditions, postconditions, invariants) et les programmes sont décorés
avec des preuves de ces assertions. Toute cette information statique est
transparente dans le sens où le comportement calculatoire n'est pas affecté
pas sa présence. Cela est dû à une procédure d'extraction intégrée qui enlève
l'information statique.

Nous illustrons aussi les principales caractéristiques de ICC* sur des
exemples classiques de programmes avec types dépendants.

Ce travail est en collaboration avec Bruno Barras.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Programming in the Calculus of Constructions is quite verbose since programs
carry static information (proof objects, dependencies, type decorations) that
is not needed in the computation. Alexandre Miquel defined a Curry-style
Implicit Calculus of Constructions (ICC) where static information does not
appear. However this system has an undecidable typechecking.

In this talk we introduce a more verbose variant, called ICC$^*$ which fixes
this issue. Datatypes and program specifications are enriched with logical
assertions (such as preconditions, postconditions, invariants) and programs
are decorated with proofs of those assertions. All of the static information
is transparent, in the sense that it does not affect the computational
behavior. This is concretized by a built-in extraction procedure that removes
this static information. We also illustrate the main features of ICC$^*$ on
classical examples of dependently typed programs.

This is joint work with Bruno Barras.