Habilitation à diriger les recherches


Soutenance

   7 décembre 2005 à 14h
   salle 79 du bâtiment 490 du campus d'Orsay (accès)

Commission d'examen

    Philippe de Groote, INRIA-Nancy    (Rapporteurs)
    Jean-Louis Krivine, PPS, U. Paris 7
    Gordon Plotkin, LFCS, U. d'Édimbourg
    Stefano Berardi, U. de Turin    (Examinateurs)
    Andrzej Filinski, DIKU, U. de Copenhague
    Christine Paulin, LRI, U. Paris 11

Mémoire principal

    C'est maintenant qu'on calcule, au cœur de la dualité
    Version révisée (corrige la section sur les types intersection et union, novembre 2008; corrige la section sur le typage appel-par-nom du calcul lambda-bar avec liaison dynamique, janvier 2010; corrige de petites erreurs de la section sur le typage appel-par-valeur du calcul lambda-bar avec liaison dynamique, juin 2007).


Exposé de soutenance (corrections typographiques incluses)

version interactive (nécessite Active Dvi)
version imprimable (format PDF)

Contenu de l'exposé

   - au cœur du calcul: le sous-système mu-mu-tilde,
   - la dualité terme / contexte d'évaluation,
   - la dualité appel par valeur / appel par nom,
   - quelle dualité pour l'appel paresseux ?
   - une dualité syntaxique inductive / coinductive,
   - les conséquences de la dualité sur la théorie de l'appel par valeur,
   - l'interprétation calculatoire du calcul des séquents,
   - un soupçon de jeux, un autre de machines à environnements
   - les limites de la dualité: coupures croisées, types dépendants, ...