Skip to Main content


Number of documents


Julien Narboux

Journal articles10 documents

Conference papers22 documents

  • Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar. Semantic parsing of geometry statements using supervised machine learning on synthetic data. NatFoM 2021 - CICM Workshop, Peter Koepke, Bonn; Dennis Müller, Erlangen, Jul 2021, Timisoara, Romania. ⟨hal-03327994⟩
  • Predrag Janičić, Julien Narboux. Automated Generation of Illustrations for Synthetic Geometry Proofs. Automated Deduction in Geometry, Zoltán Kovács, Sep 2021, Hagenberg, Austria. ⟨hal-03327987⟩
  • Charly Gries, Julien Narboux, Pierre Boutry. Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq. Journées Francophones des Langages Applicatifs 2019, Jan 2019, Les Rousses, France. ⟨hal-01923814v2⟩
  • Pierre Boutry, Gabriel Braun, Julien Narboux. From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry. SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan. pp.14-28. ⟨hal-01282550⟩
  • Charly Gries, Pierre Boutry, Julien Narboux. Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq. Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jade Algave; Julien Signoles, Jan 2016, Saint Malo, France. pp.15. ⟨hal-01228612v2⟩
  • Gabriel Braun, Pierre Boutry, Julien Narboux. From Hilbert to Tarski. Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19. ⟨hal-01332044⟩
  • Sana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic. A Vernacular for Coherent Logic. CICM 2014 - Conferences on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. pp.16, ⟨10.1007/978-3-319-08434-3_28⟩. ⟨hal-00983975v2⟩
  • Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. A short note about case distinctions in Tarski's geometry. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15. ⟨hal-00989785v2⟩
  • Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. Using small scale automation to improve both accessibility and readability of formal proofs in geometry. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-19. ⟨hal-00989781v2⟩
  • Pascal Schreck, Pascal Mathis, Julien Narboux. Geometric Construction Problem Solving in Computer-Aided Learning. 24th IEEE International Conference on Tools with Artificial Intelligence, Nov 2012, Athens, Greece. pp.1139 - 1144, ⟨10.1109/ICTAI.2012.162⟩. ⟨hal-00753551⟩
  • Gabriel Braun, Julien Narboux. From Tarski to Hilbert. Automated Deduction in Geometry 2012, Jacques Fleuriot, Sep 2012, Edinburgh, United Kingdom. pp.89-109, ⟨10.1007/978-3-642-40672-0_7⟩. ⟨hal-00727117v2⟩
  • Bruno Cuervo Parrino, Julien Narboux, Eric Violard, Nicolas Magaud. Dealing with arithmetic overflows in the polyhedral model. IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Louis-Noel Pouchet, Jan 2012, Paris, France. ⟨hal-00655485⟩
  • Jean-David Génevaux, Julien Narboux, Pascal Schreck. Formalization of Wu's simple method in Coq. CPP 2011 First International Conference on Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. pp.71-86, ⟨10.1007/978-3-642-25379-9_8⟩. ⟨inria-00618745v2⟩
  • Tuan Minh Pham, Yves Bertot, Julien Narboux. A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry. The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Jun 2011, Santander, Spain. pp.368-383, ⟨10.1007/978-3-642-21898-9_32⟩. ⟨inria-00584918⟩
  • Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Desargues' theorem in Coq using ranks in Coq. 24th Annual ACM Symposium on Applied Computing, Xiao-Shan Gao, Robert Joan-Arinyo, Dominique Michelucci, Mar 2009, Honolulu, United States. pp.1110-1115, ⟨10.1145/1529282.1529527⟩. ⟨inria-00335719⟩
  • Christian Urban, Julien Narboux. Formal SOS-Proofs for the Lambda-Calculus. Third Workshop on Logical and Semantic Frameworks, with Applications, Mauricio Ayala-Rincón, Aug 2008, Salvador, Brazil. pp.139-155, ⟨10.1016/j.entcs.2009.07.053⟩. ⟨inria-00335718⟩
  • Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Projective Plane Geometry in Coq. Post-proceedings of Automated Deduction in Geometry (ADG) 2008, Thomas Sturm, Sep 2008, Shanghai, China. pp.141-162, ⟨10.1007/978-3-642-21046-4⟩. ⟨inria-00305998v3⟩
  • Julien Narboux. GeoProof: A user interface for formal proofs in geometry. MathUI 07, Jun 2007, Linz, Austria. ⟨inria-00495958⟩
  • Julien Narboux, Christian Urban. Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.. LFMTP'07, Jul 2007, Bremen, Germany. 15p., ⟨10.1016/j.entcs.2007.09.014⟩. ⟨inria-00180061v2⟩
  • Julien Narboux. Mechanical Theorem Proving in Tarski's geometry.. Automated Deduction in Geometry 2006, Francisco Botana, Aug 2006, Pontevedra, Spain. pp.139-156, ⟨10.1007/978-3-540-77356-6⟩. ⟨inria-00118812⟩
  • Julien Narboux. Toward the use of a proof assistant to teach mathematics. The Seventh International Conference on Technology in Mathematics Teaching (ICTMT7), Jul 2005, Bristol, United Kingdom. ⟨inria-00495952⟩
  • Julien Narboux. A Decision Procedure for Geometry in Coq. Theorem Proving in Higher Order Logics 2004, Jul 2004, Park City, USA, United States. pp.225-240, ⟨10.1007/b100400⟩. ⟨inria-00001035⟩

Book sections2 documents

  • Julien Narboux, Viviane Durand-Guerrier. Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. Mathematics Education in the Age of Artificial Intelligence: How Intelligence can serve mathematical human learning, Springer, 2021. ⟨hal-03254579⟩
  • Julien Narboux, Predrag Janicic, Jacques Fleuriot. Computer-assisted Theorem Proving in Synthetic Geometry. Meera Sitharam; Audrey St. John; Jessica Sidman. Handbook of Geometric Constraint Systems Principles, Chapman and Hall/CRC , In press, Discrete Mathematics and Its Applications, 1498738915. ⟨hal-01779452⟩

Directions of work or proceedings2 documents

  • Julien Narboux, Pascal Schreck, Ileana Streinu. Proceedings of ADG 2016: Eleventh International Workshop on Automated Deduction in Geometry. Jun 2016, Strasbourg, France. pp.224, 2016. ⟨hal-01334334⟩
  • Julien Narboux, Schreck Pascal, Jürgen Richter-Gebert. Automated Deduction in Geometry - 8th International Workshop, Revised Selected Papers. Pascal Schreck and Julien Narboux and Jürgen Richter-Gebert. France. 6877, Springer, pp.258, 2011, Lecture Notes in Computer Science, 978-3-642-25069-9. ⟨10.1007/978-3-642-25070-5⟩. ⟨hal-00644313⟩

Preprints, Working Papers, ...2 documents

  • Pierre Boutry, Julien Narboux, Pascal Schreck. A reflexive tactic for automated generation of proofs of incidence to an affine variety. 2015. ⟨hal-01216750⟩
  • Julien Narboux. A formalization of diagrammatic proofs in abstract rewriting. 2006. ⟨inria-00180065⟩

Theses1 document

  • Julien Narboux. Formalisation et automatisation du raisonnement géométrique en Coq.. Autre [cs.OH]. Université Paris Sud - Paris XI, 2006. Français. ⟨tel-00118806⟩