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, logiciels 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:

• membre du bureau éditorial du Journal of Functional Programming;
• organisateur du séminaire de notre équipe;
• président du comité de suivi des doctorants de l'Inria Paris.

Événements prochains:

• ICFP 2019 (président du comité de programmes; je serai présent).

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, une bibliothèque OCaml pour la mémoisation, le hash-consing, et le calcul de plus petit points fixes;
• PPrint, une adaptation à OCaml du bel afficheur de Wadler et Leijen;
• 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;
• (2013) dblib, une librairie Coq pour gérer la liaison et les indices de de Bruijn (README) (archive);
• (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:

• Frédéric Bour (2019-) (également chercheur chez Facebook),
• Glen Mével (2018-) (co-encadré avec Jacques-Henri Jourdan),
• Naomi Testard (2017-2019),
• 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.