Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Hugo.Herbelin@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Coq - 21/04/2000 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E

   ____              ____    .                   
  /   _   _        /    ___   __  /_  _   /     /| /|  _   __ __ _       _ 
 /   / \ / \  _   /    /   / /_  /   __| /  _  / |/ | / \ /_ /  / \ | / __|
|___ |_/ |_/     |___ /   / __/ |_  |_/ |_    /     | |_/__/ |_ |_/ |/ |_/
          /                                                                 
         /                                                                  
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 11

                          Vendredi 21 avril, 10h30

                            -------------------
                            Pierre-Louis Curien
                            -------------------

                          PPS - Université Paris 7

                          ========================
                          Sur la dualité du calcul
                          ========================

(travail en collaboration avec Hugo Herbelin)

Nous présentons le lambdabar-mu-mu~-calcul, une syntaxe pour
le lambda-calcul avec opérateur de contrôle et "let-in" qui exhibe des
symétries de calcul telles que programme/contexte et appel par
nom/appel par valeur (le lambdabar-mu-mu~-calcul est dérivé du calcul
des séquents LK, un formalisme clé de la théorie de la démonstration).

Dans notre syntaxe, choisir la discipline appel par nom/appel par
valeur pour la réduction se ramène à choisir l'une des deux
orientations symétriques d'une paire critique (qui est une version
polarisée de celle du lambda-calcul symétrique du Berardi et
Barbanera). Notre analyse nous conduit a revisiter la question de
savoir ce qu'est une syntaxe naturelle fonctionnelle pour le calcul
par valeur.

Nous définissons une traduction du lambda-mu-calcul dans le
lambdabar-mu-mu~-calcul et deux traductions du lambdabar-mu-mu~-calcul
dans le lambda-calcul. En composant ces traductions, nous retrouvons
des traductions CPS connues pour l'appel par valeur et l'appel par nom.

Enfin, nous nous intéresserons aux machines abstraites pour le
lambdabar-mu-mu~-calcul.