


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:
Enseignement:
Activités:
Événements prochains:
- ESOP 2019
(je ne serai pas présent, mais Glen présentera notre travail).
- 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
(code source,
documentation),
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-),
- 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: