Publications

• PhD Une Théorie des Constructions Inductives, Université Paris 7, 1994.
• On the Church-Rosser Property for Expressive Types Systems and its Consequences for their Metatheoretic Study. With Herman Geuvers. LICS 1994. bibtex
• Synthesis of ML Programs in the System Coq. With Christine Paulin-Mohring. Journal of Symbolic Computation, 1993. bibtex
• A Generic Normalization Proof for Pure Type Systems. With Paul-André Melliès. TYPES 1996 (LNCS 1512).As INRIA report bibtex 
• Proof Normalization Modulo. With Gilles Dowek. Journal of Symbolic Logic, 2003. bibtexpdf draft. A first version appeared in TYPES 1998 (LNCS 1657). 
• Sets in Types, Types in Sets. TACS 1997 (LNCS 1281). bibtex Springer pdf pdf draft
• The not-so-simple proof-irrelevant model of CC. With Alexandre Miquel. TYPES 2002 (LNCS 2646). pdf draft Springer pdf bibtex 
• Choice in Dynamic Linking. With Martin Abadi and Georges Gonthier. FOSSACS 2004 (LNCS 2987). bibtex Springer pdf
• Arithmetic as a Theory Modulo. With Gilles Dowek. RTA 2005 (LNCS 3467). pdf draft bibtex springer pdf
• A computational Approach to Pocklington Certificates in Type Theory. With Benjamin Grégoire and Laurent Théry. FLOPS 2006 (LNCS 3945). pdf draft bibtex Springer pdf
• On the Strength of Proof-Irrelevant Type Theories. IJCAR 2006 (LNAI, LNCS 4130). pdf draft, Springer pdf, draft of longer version: pdf.
• La Vérité et la Machine. Images des Mathématiques 2006. CNRS. pdf
• Simple Types in Type Theory: deep and shallow encodings. With François Garillot. TPHOLs 2007; pdf draft.

The red links will only work if your institution bought the right to download from the publisher's site

Other writings

• Variations on a theme by Diaconescu. With Samuel Lacas.
• The eta-long normal form for type systems of the cube. With Gilles Dowek and Gérard Huet.