A Decision Procedure for Geometry in Coq. - Julien Narboux (TPHOLs, 2004)

Mechanical Theorem Proving in Tarski's Geometry. - Julien Narboux (Automated Deduction in Geometry, 2006)

Formalisation et automatisation du raisonnement géométrique en Coq. (Formalisation and automation of geometric reasoning within Coq). - Julien Narboux (2006)

Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. - Julien Narboux; Christian Urban (LFMTP@CADE, 2007)

A Graphical User Interface for Formal Proofs in Geometry. - Julien Narboux (J. Autom. Reason., 2007)

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

Formal SOS-Proofs for the Lambda-Calculus. - Christian Urban; Julien Narboux (LSFA, 2008)

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

Formalization of Wu's Simple Method in Coq. - Jean-David Génevaux; Julien Narboux; Pascal Schreck (CPP, 2011)

A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. - Tuan-Minh Pham; Yves Bertot; Julien Narboux (ICCSA (4), 2011)

From Tarski to Hilbert. - Gabriel Braun; Julien Narboux (Automated Deduction in Geometry, 2012)

Geometric Construction Problem Solving in Computer-Aided Learning. - Pascal Schreck; Pascal Mathis; Julien Narboux (ICTAI, 2012)

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

The Area Method - A Recapitulation. - Predrag Janicic; Julien Narboux; Pedro Quaresma (J. Autom. Reason., 2012)

A Vernacular for Coherent Logic. - Sana Stojanovic; Julien Narboux; Marc Bezem; Predrag Janicic (CICM, 2014)

Automated generation of machine verifiable and readable proofs: A case study of Tarski's geometry. - Sana Stojanovic Durdevic; Julien Narboux; Predrag Janicic (Ann. Math. Artif. Intell., 2015)

Herbrand's Theorem and non-Euclidean Geometry. - Michael Beeson; Pierre Boutry; Julien Narboux (Bull. Symb. Log., 2015)

From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry. - Pierre Boutry; Gabriel Braun; Julien Narboux (SCSS, 2016)

Towards a Certified Version of the Encyclopedia of Triangle Centers. - Julien Narboux; David Braun (Math. Comput. Sci., 2016)

A Synthetic Proof of Pappus' Theorem in Tarski's Geometry. - Gabriel Braun; Julien Narboux (J. Autom. Reason., 2017)

Proof-checking Euclid. - Michael Beeson; Julien Narboux; Freek Wiedijk (Ann. Math. Artif. Intell., 2019)

Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq. - Pierre Boutry; Charly Gries; Julien Narboux; Pascal Schreck (J. Autom. Reason., 2019)

Formalization of the arithmetization of Euclidean plane geometry and applications. - Pierre Boutry; Gabriel Braun; Julien Narboux (J. Symb. Comput., 2019)

Semantic parsing of geometry statements using supervised machine learning on synthetic data. - Salwa Tabet Gonzalez; Stéphane Graham-Lengrand; Julien Narboux; Natarajan Shankar (CICM Workshops, 2021)

Automated Generation of Illustrations for Synthetic Geometry Proofs. - Predrag Janicic; Julien Narboux (ADG, 2021)

Theorem Proving as Constraint Solving with Coherent Logic. - Predrag Janicic; Julien Narboux (J. Autom. Reason., 2022)

Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving. - Salwa Tabet Gonzalez; Predrag Janicic; Julien Narboux (ADG, 2023)

Automated generation of illustrated proofs in geometry and beyond. - Predrag Janicic; Julien Narboux (Ann. Math. Artif. Intell., 2023)

Proof Assistants for Teaching: a Survey. - Frédéric Tran Minh; Laure Gonnord; Julien Narboux (ThEdu@CADE, 2024)