


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:
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:
Photos: