Je suis directeur de recherche à l'INRIA à Paris. (Voici des indications pour nous rendre visite, et voici une carte.) Je suis membre de l'équipe Gallium.

Those who would give up essential Liberty, to purchase a little temporary Safety, deserve neither Liberty nor Safety. -- Benjamin Franklin (1755)

Recherche:

• la liste de mes publications et exposés;
• les articles que j'ai cités permettent d'identifier mes intérêts (fichier .bib);

Enseignement:

• j'enseigne une partie du cours programmation fonctionnelle et systèmes de types (2-4) (2-4) au MPRI;
• J'ai enseigné à l'École Polytechnique. Le matériel des deux cours suivants reste disponible en ligne:
  • compilation (INF564);
  • «programmation avancée» (INF441) en Java et OCaml.

Activités:

• Journal of Functional Programming (membre du bureau éditorial);
• le séminaire de notre équipe (organisateur).

Événements prochains:

• IFIP 2.16 Working Group on Language Design.
• ICFP 2018 (membre du comité de programmes).
• ICFP 2019 (président du comité de programmes).

Logiciels à jour (gitlab):

• Menhir, un générateur d'analyseurs syntaxiques LR(1) pour le langage de programmation OCaml;
• visitors, une extension de syntaxe OCaml qui engendre des visiteurs orientés objets pour traverser et transformer des structures de données (documentation);
• Inferno, une bibliothèque OCaml pour l'inférence de types ML et l'élaboration, décrite dans mon article ICFP 2014.
• Fix, un module OCaml simple permettant de calculer le plus petit point fixe d'un système d'équations monotones;
• PPrint (code source, documentation), une adaptation à OCaml du bel afficheur de Wadler et Leijen;
• dblib, une librairie Coq pour gérer la liaison et les indices de de Bruijn (README) (archive);
• loop, une librairie Coq pour écrire une boucle do/while, tout en produisant un code extrait propre en OCaml.

Logiciels moins à jour:

• (2014) Mezzo, un langage de programmation expérimental que j'ai développé avec Jonathan Protzenko;
• (2010) FORK, une extension du Système F Omega avec des sortes récursives bien élevées (en anglais);
• (2009) mon joueur de Puissance 4;
• (2007) Pure FreshML, un langage de programmation prototype avec lequel j'ai joué (en anglais);
• (2006) Cαml, un outil qui facilite la gestion de l'α-conversion dans les programmes OCaml;
• (2006) une implémentation prototype du chapitre The Essence of ML Type Inference, par Yann Régis-Gianas, Didier Rémy, et moi-même;
• (2001) mon modeste joueur de morpion;
• (2000) Wallace, une bibliothèque pour engendrer et simplifier des contraintes de sous-typage;
• (2000) mon vérificateur de liens Web Big Brother;
• (1998) mes logiciels Macintosh.

Mes étudiants en thèse présents et passés sont:

• Leo Testard (2017-),
• Armaël Guéneau (2016-) (co-encadré avec Arthur Charguéraud),
• Jonathan Protzenko (2010-2014) (aujourd'hui chercheur chez Microsoft Research à Redmond),
• Nicolas Pouillard (2008-2011) (aujourd'hui développeur et chercheur indépendant),
• Alexandre Pilkiewicz (2008-2011) (aujourd'hui chez Google France),
• Arthur Charguéraud (2007-2010) (aujourd'hui chercheur Inria),
• Yann Régis-Gianas (2004-2007) (aujourd'hui maître de conférences à l'Université Paris Diderot),
• Nadji Gauthier (2003-2005),
• Vincent Simonet (2000-2004) (aujourd'hui chez Google France).

Photos:

• travailler la nuit dédouble ma productivité;
• l'album 2005 de ma fille Lola;
• Retour en Corse, un album avec texte et photos;
• quelques vieilles photos, maigrement commentées, de Corse, du Mercantour, et des Pyrénées;
• la gestuelle de mon profs de maths à l'ENS, vers 1993.