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'ai enseigné à l'École Polytechnique. Le matériel des deux cours suivants reste disponible en ligne:
Activités:
- Journal of Functional Programming (membre du bureau éditorial);
- le séminaire de notre équipe (organisateur).
Événements prochains:
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.
 | Page principale | Dernière modification : 07 June 2017 |