I am a senior researcher at INRIA in Paris, France. (Here are directions to our site, and here is a map.) I lead the Cambium team.
Quotes:- 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
- lists of my publications, software, and talks;
- the papers I have cited define my interests (.bib file);
Teaching:
- I teach part of (and am the head of) the course on functional programming and type systems (2-4) at MPRI;
- I once taught at École Polytechnique. The material for the following two courses remains available:
Activities:
- organizer of our group's seminar;
- in charge of the PhD committee (CSD) at Inria Paris.
Upcoming events:
Current software (gitlab):
- Menhir, an LR(1) parser generator for the OCaml programming language (documentation) (mailing list);
- Sek, an OCaml library that offers efficient ephemeral and persistent sequences, co-authored with Arthur Charguéraud (documentation);
- Monolith, a tool that helps perform random testing or fuzz testing of an arbitrary OCaml library (documentation);
- Visitors, an OCaml syntax extension that generates object-oriented visitors for traversing and transforming data structures (documentation);
- Inferno, an OCaml library for ML type inference and elaboration, described in my ICFP 2014 paper (documentation) (mailing list);
- Fix, an OCaml library for memoization, hash-consing, and computing least fixed points (documentation);
- PPrint, an OCaml adaptation of Wadler's and Leijen's prettier printer (documentation);
- Feat, an OCaml library for counting, enumerating and sampling inhabitants of algebraic data types (documentation);
- UnionFind, an OCaml library that offers several implementations of this famous data structure (documentation);
- Loop, a Coq library for writing a do/while loop, while producing clean OCaml extracted code.
Not-so-current software:
- (2014) Mezzo, a prototype programming language that I have developed together with Jonathan Protzenko;
- (2013) dblib, a Coq library for dealing with binding using de Bruijn indices (README) (archive);
- (2010) FORK, an extension of System F Omega with well-behaved Recursive Kinds;
- (2009) my Connect 4 player;
- (2007) Pure FreshML, a prototype programming language that I have toyed with;
- (2006) Cαml, a tool that helps deal with α-conversion in OCaml programs;
- (2006) a prototype implementation for the book chapter The Essence of ML Type Inference, by Yann Régis-Gianas, Didier Rémy, and myself;
- (2001) my simple-minded 5-in-a-row player;
- (2000) Wallace, a library for generating and simplifying subtyping constraints;
- (2000) my World Wide Web link checker Big Brother;
- (1998) my Macintosh software.
My current and former Ph.D. students are:
- Remy Seassau (2023-),
- Tiago Soares (2023-) (co-advised by myself and by Mário Pereira),
- Clément Allain (2022-),
- Alexandre Moine (2021-) (co-advised by myself and by Arthur Charguéraud),
- Olivier Martinot (2020-) co, (co-advised by myself and by Gabriel Scherer),
- Paulo Emílio de Vilhena (2019-2022) (now a postdoctoral researcher at Imperial College London),
- Frédéric Bour (2019-) (also an engineer at Tarides),
- Glen Mével (2018-2022) (co-advised by myself and by Jacques-Henri Jourdan),
- Naomi Testard (2017-2019),
- Armaël Guéneau (2016-2019) (co-advised by myself and by Arthur Charguéraud) (now a researcher at Inria Saclay),
- Jonathan Protzenko (2010-2014) (now a researcher at Microsoft Research in Redmond),
- Nicolas Pouillard (2008-2011) (now a free-lance programmer and researcher),
- Alexandre Pilkiewicz (2008-2011) (now at Google France),
- Arthur Charguéraud (2007-2010) (now a researcher at Inria in Strasbourg),
- Yann Régis-Gianas (2004-2007) (now at Nomadic Labs),
- Nadji Gauthier (2003-2005),
- Vincent Simonet (2000-2004) (now at Google France).
Photos:
- working at night doubles my productivity;
- my daughter Lola's 2005 album;
- Back to Corsica, an album with text and photos;
- older, sparsely commented photos of Corsica, Mercantour, and Pyrénées;
- the body language of my math teacher at ENS, around 1993 (in French).
Leisure:
- I am a member (and the webmaster) of the Choucas Cellois, a mountain biking club West of Paris.
