Changing Data Structures in Type Theory: A Study of Natural Numbers. - Nicolas Magaud; Yves Bertot (TYPES, 2000)

Changement de représentation des structures de données en Coq: le cas des entiers naturels. - Nicolas Magaud; Yves Bertot (JFLA, 2001)

A Proof of GMP Square Root. - Yves Bertot; Nicolas Magaud; Paul Zimmermann (J. Autom. Reason., 2002)

Changing Data Representation within the Coq System. - Nicolas Magaud (TPHOLs, 2003)

Changements de Représentation des Données dans le Calcul des Constructions. (Changing Data Representation in the Calculus of Constructions). - Nicolas Magaud (2003)

Formalizing Projective Plane Geometry in Coq. - Nicolas Magaud; Julien Narboux; Pascal Schreck (Automated Deduction in Geometry, 2008)

Formalizing Desargues' theorem in Coq using ranks. - Nicolas Magaud; Julien Narboux; Pascal Schreck (SAC, 2009)

Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. - Christophe Brun; Jean-François Dufourd; Nicolas Magaud (Automated Deduction in Geometry, 2012)

Designing and proving correct a convex hull algorithm with hypermaps in Coq. - Christophe Brun; Jean-François Dufourd; Nicolas Magaud (Comput. Geom., 2012)

A case study in formalizing projective geometry in Coq: Desargues theorem. - Nicolas Magaud; Julien Narboux; Pascal Schreck (Comput. Geom., 2012)

Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. - Nicolas Magaud; Agathe Chollet; Laurent Fuchs (Ann. Math. Artif. Intell., 2015)

Formalizing Some "Small" Finite Models of Projective Geometry in Coq. - David Braun; Nicolas Magaud; Pascal Schreck (AISC, 2018)

Two cryptomorphic formalizations of projective incidence geometry. - David Braun; Nicolas Magaud; Pascal Schreck (Ann. Math. Artif. Intell., 2019)

Contributions au développement des méthodes formelles de preuves et applications à la géométrie. - Nicolas Magaud (2020)

Two New Ways to Formally Prove Dandelin-Gallucci's Theorem. - David Braun; Nicolas Magaud; Pascal Schreck (ISSAC, 2021)

Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant. - Nicolas Magaud (PxTP, 2021)

Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach. - Pascal Schreck; Nicolas Magaud; David Braun (ADG, 2021)

Spreads and Packings of PG(3, 2), Formally! - Nicolas Magaud (ADG, 2021)

Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant. - Nicolas Magaud (ITP, 2022)

Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. - Catherine Dubois; Nicolas Magaud; Alain Giorgetti (TYPES, 2022)

Some representations of real numbers using integer sequences. - Loïc Mazo; Marie-Andrée Jacob-Da Col; Laurent Fuchs; Nicolas Magaud; Gaëlle Skapin (Math. Struct. Comput. Sci., 2022)

Towards Automatic Transformations of Coq Proof Scripts. - Nicolas Magaud (ADG, 2023)

A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry. - David Braun; Nicolas Magaud; Pascal Schreck (J. Autom. Reason., 2024)