Formalizing Stålmarck's Algorithm in Coq. - Pierre Letouzey; Laurent Théry (TPHOLs, 2000)

A New Extraction for Coq. - Pierre Letouzey (TYPES, 2002)

Functors for Proofs and Programs. - Jean-Christophe Filliâtre; Pierre Letouzey (ESOP, 2004)

Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant). - Pierre Letouzey (2004)

A Large-Scale Experiment in Executing Extracted Programs. - Luís Cruz-Filipe; Pierre Letouzey (Calculemus, 2005)

Coq. - Laurent Théry; Pierre Letouzey; Georges Gonthier (The Seventeen Provers of the World, 2006)

Program Extraction from Normalization Proofs. - Ulrich Berger 001; Stefan Berghofer; Pierre Letouzey; Helmut Schwichtenberg (Stud Logica, 2006)

Extraction in Coq: An Overview. - Pierre Letouzey (CiE, 2008)

Hofstadter's problem for curious readers. - Pierre Letouzey (CoRR, 2015)

Pointwise order of generalized Hofstadter functions G, H and beyond. - Pierre Letouzey; Shuo Li; Wolfgang Steiner (CoRR, 2024)

Generalized Hostadter functions G, H and beyond: numeration systems and discrepancy. - Pierre Letouzey (CoRR, 2025)