To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 20/04/09 - 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 20 avril, 14h30

                               --------------
                               Benoît Valiron
                               --------------

                                    LIX

                    ===================================
                    Ordre supérieur en calcul quantique
                    ===================================

En calcul quantique, le type de base est le booléen quantique. Il possède
plusieurs propriétés particulières. Il est non-duplicable, il peut se trouver
en superposition, et la mesure, seule opération répondant à la question "quel
est son état?", est non seulement probabiliste mais modifie l'état en
question.

À travers l'étude de l'algorithme de téléportation quantique, nous discuterons
de l'intérêt d'une interprétation fonctionnelle et d'ordre supérieur du calcul
quantique.

Nous décrirons ensuite un lambda-calcul pour le calcul quantique muni d'un
système de types basé sur la logique linéaire afin de différencier les données
duplicables des données non-duplicables. Nous détaillerons les difficultés qui
surgissent lors de la construction d'une sémantique opérationnelle.

Finalement, à l'aide d'une sémantique catégorielle, nous développerons un
modèle dénotationnel pour décrire la structure logique inhérente au langage
développé. Nous évoquerons les pistes de recherche en vue de trouver des
modèles concrets pour ce langage et pour le relier aux modèles de preuves de
la logique linéaire.