


Je suis directeur de recherche à l'INRIA à Paris.
(Voici des indications pour nous rendre visite, et voici une carte.)
Je suis responsable de l'équipe Cambium.
Citations:
- Those who would give up essential Liberty, to purchase a little
temporary Safety, deserve neither Liberty nor Safety.
-- Benjamin Franklin (1755)
- Beaucoup de mal durable est souvent fait par les choses provisoires.
-- Victor Hugo (1848)
- Chacun appelle idées claires celles qui sont au même degré de confusion que les siennes propres.
-- Marcel Proust
- Tough ain't enough.
-- Frankie
- Remind me to come here next time I want my constitution undermined.
-- Egbert
Recherche:
Enseignement:
Activités:
Événements prochains:
Logiciels à jour (gitlab):
- Menhir, un générateur d'analyseurs syntaxiques LR(1)
pour le langage de programmation OCaml
(documentation)
(mailing list);
- Sek,
une bibliothèque OCaml
qui propose des séquences éphémères et persistantes efficaces,
co-écrite avec Arthur Charguéraud
(documentation);
- Monolith,
un outil qui facilite le test par fuzzing d'une bibliothèque OCaml quelconque
(documentation);
- 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
(documentation)
(mailing list);
- Fix,
une bibliothèque OCaml pour la mémoisation, le hash-consing,
et le calcul de plus petit points fixes
(documentation);
- PPrint,
une adaptation à OCaml du bel afficheur de Wadler et Leijen
(documentation);
- Feat,
une bibliothèque OCaml pour compter, énumérer et échantillonner
les habitants d'un type algébrique
(documentation);
- UnionFind,
une bibliothèque OCaml qui propose plusieurs implémentations de cette célèbre structure de données
(documentation);
- 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:
- Clément Allain (2022-),
- Alexandre Moine (2021-)
(co-encadré avec Arthur Charguéraud),
- Olivier Martinot (2020-),
- Paulo Emílio de Vilhena (2019-2022)
(aujourd'hui en postdoc à Imperial College London),
- Frédéric Bour (2019-)
(également ingénieur chez Tarides),
- Glen Mével (2018-2022)
(co-encadré avec Jacques-Henri Jourdan),
- Naomi Testard (2017-2019),
- Armaël Guéneau (2016-2019)
(co-encadré avec Arthur Charguéraud)
(aujourd'hui chercheur à l'Inria Saclay),
- 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 à l'Inria Strasbourg),
- Yann Régis-Gianas (2004-2007)
(aujourd'hui chez Nomadic Labs),
- Nadji Gauthier (2003-2005),
- Vincent Simonet (2000-2004)
(aujourd'hui chez Google France).
Photos:
Loisirs:
- Je suis membre (et webmestre) des Choucas Cellois,
un club VTT situé à l'Ouest de Paris.