Normalisation by Completeness with Heyting Algebras. - Gaëtan Gilbert; Olivier Hermant (LPAR, 2015)

Design and Implementation of the Andromeda Proof Assistant. - Andrej Bauer; Gaëtan Gilbert; Philipp G. Haselwarter; Matija Pretnar; Christopher A. Stone (TYPES, 2016)

Formalising real numbers in homotopy type theory. - Gaëtan Gilbert (CPP, 2017)

Definitional proof-irrelevance without K. - Gaëtan Gilbert; Jesper Cockx; Matthieu Sozeau; Nicolas Tabareau (Proc. ACM Program. Lang., 2019)

A type theory with definitional proof-irrelevance. (Une théorie des types avec insignifiance des preuves définitionnelle). - Gaëtan Gilbert (2019)

Extending the team with a project-specific bot. - Théo Zimmermann; Julien Coolen; Jason Gross; Pierre-Marie Pédrot; Gaëtan Gilbert (CoRR, 2021)

Advantages of maintaining a multi-task project-specific bot: an experience report. - Théo Zimmermann; Julien Coolen; Jason Gross; Pierre-Marie Pédrot; Gaëtan Gilbert (CoRR, 2022)

The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report. - Théo Zimmermann; Julien Coolen; Jason Gross; Pierre-Marie Pédrot; Gaëtan Gilbert (IEEE Softw., 2022)

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. - Yann Leray; Gaëtan Gilbert; Nicolas Tabareau; Théo Winterhalter (ITP, 2024)

All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. - Josselin Poiret; Gaëtan Gilbert; Kenji Maillard; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2025)