2024

Journal articles

ref_biblio

Adrien Krähenbühl, Julien Narboux, Basile Sauvage. Le cuisinier pressé. Tangente Éducation, 2024, L'informatique débranchée Tome 2, Activités en parallélisme, sécurité, et intelligence artificielle, 67-68, pp.34-37. ⟨hal-04694095⟩

Accès au bibtex

Conference papers

ref_biblio

Frédéric Tran Minh, Laure Gonnord, Julien Narboux. Proof assistants for teaching: a survey. The 13th International Workshop on Theorem proving components for Educational software (ThEdu 24), Jul 2024, Nancy, France. ⟨hal-04705596⟩

Accès au bibtex

Proceedings

ref_biblio

Julien Narboux, Walther Neuper, Pedro Quaresma. Proceedings 12th International Workshop on Theorem proving components for Educational software. 12th International Workshop on Theorem proving components for Educational software, Electronic Proceedings in Theoretical Computer Science, 400, EPTCS, 2024, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/eptcs.400⟩. ⟨hal-04537213⟩

Accès au texte intégral et bibtex

Reports

ref_biblio

Frédéric Tran Minh, Laure Gonnord, Julien Narboux. Research report - Proof assistants for teaching: a survey. LCIS, Grenoble-INP. 2024. ⟨hal-04705580⟩

Accès au texte intégral et bibtex

2023

Journal articles

ref_biblio

Predrag Janičić, Julien Narboux. Automated generation of illustrated proofs in geometry and beyond. Annals of Mathematics and Artificial Intelligence, 2023, https://link.springer.com/article/10.1007/s10472-023-09857-y. ⟨10.1007/s10472-023-09857-y⟩. ⟨hal-04230795⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux. Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving. Automated Deduction in Geometry 2023, Vesna Marinkovic; Danijela Simić; Sana Stojanović Đurđević; Milan Banković, Sep 2023, Belgrade, Serbia. ⟨hal-04226900⟩

Accès au texte intégral et bibtex

ref_biblio

Julien Narboux. Formalisation, arithmetization and automatisation of geometry. Automated Deduction in Geometry 2023, Predrag Janičić; Pedro Quaresma; Zoltán Kovács; Vesna Marinković, Sep 2023, Belgrade, France. ⟨hal-04226945⟩

Accès au bibtex

ref_biblio

Pierre Boutry, Julien Narboux. Tutorial Laboratory - GeoCoq to formalize high-school geometry problems. ADG 2023 - Automated Deduction in Geometry 2023, Predrag Janičić; Pedro Quaresma; Zoltán Kovács, Sep 2023, Belgrade, Serbia. ⟨hal-04230732⟩

Accès au texte intégral et bibtex

ref_biblio

Evmorfia-Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux. Underlying theories of proof assistants and potential impact on the teaching and learning of proof. 12th International Workshop on Theorem proving components for Educational software, Julien Narboux; Walther Neuper; Pedro Quaresma, Jul 2023, Rome, Italy. ⟨hal-04227823⟩

Accès au bibtex

Preprints, Working Papers, ...

ref_biblio

Evmorfia-Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux. Proof assistants for undergraduate mathematics education: elements of an a priori analysis. 2023. ⟨hal-04087080⟩

Accès au texte intégral et bibtex

2022

Journal articles

ref_biblio

Predrag Janičić, Julien Narboux. Theorem Proving as Constraint Solving with Coherent Logic. Journal of Automated Reasoning, 2022, 66 (4), pp.689-746. ⟨10.1007/s10817-022-09629-z⟩. ⟨hal-03632665⟩

Accès au texte intégral et bibtex

ref_biblio

Marie Kerjean, Frédéric Le Roux, Patrick Massot, Micaela Mayero, Zoé Mesnil, et al.. Utilisation des assistants de preuves pour l’enseignement en L1. La Gazette de la Société mathématique de France, 2022, 174. ⟨hal-03979238⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

Evmorfia Bartzia, Antoine Meyer, Julien Narboux. Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis. INDRUM 2022: Fourth conference of the International Network for Didactic Research in University Mathematics, Reinhard Hochmuth, Oct 2022, Hanovre, Germany. pp.253-262. ⟨hal-03648357v2⟩

Accès au texte intégral et bibtex

Book sections

ref_biblio

Julien Narboux, Viviane Durand-Guerrier. Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. Richard P.R.; Vélez M.P.; Van Vaerenbergh S. Mathematics Education in the Age of Artificial Intelligence: How Intelligence can serve mathematical human learning, 17, Springer, pp.167-192, 2022, Mathematics Education in the Digital Era, 978-3-030-86908-3. ⟨10.1007/978-3-030-86909-0_8⟩. ⟨hal-03254579⟩

Accès au texte intégral et bibtex

2021

Journal articles

ref_biblio

Basile Sauvage, Jean-Christophe Grimont, Régine Hamm-Audonnet, Julien Narboux. Découvrir des concepts informatiques autour des arbres binaires, Une série d’activités d’informatique débranchée. Repères, 2021, 125. ⟨hal-03797893⟩

Accès au bibtex

ref_biblio

Julien Narboux, Cristel Pelsser, Basile Sauvage, Gaelle Thomas. La cordée de la réussite "décodeuses d'informatique". 1024 : Bulletin de la Société Informatique de France, 2021, 18, pp.87-89. ⟨10.48556/SIF.1024.18.87⟩. ⟨hal-04476335⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

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. pp.91-102, ⟨10.4204/EPTCS.352.9⟩. ⟨hal-03327987⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

2019

Journal articles

ref_biblio

Pierre Boutry, Gabriel Braun, Julien Narboux. Formalization of the Arithmetization of Euclidean Plane Geometry and Applications. Journal of Symbolic Computation, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩. ⟨hal-01483457⟩

Accès au texte intégral et bibtex

ref_biblio

Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck. Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Journal of Automated Reasoning, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩. ⟨hal-01178236v2⟩

Accès au texte intégral et bibtex

ref_biblio

Michael Beeson, Julien Narboux, Freek Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩. ⟨hal-01612807v3⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

2018

Book sections

ref_biblio

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⟩

Accès au bibtex

Software

ref_biblio

Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, Julien Narboux. GeoCoq. 2018, ⟨swh:1:dir:97ce53176b7d5e89d069bc60f49c3fa186831307;origin=https://hal.archives-ouvertes.fr/hal-01912024;visit=swh:1:snp:1cbf6e8cee9dde43b03c16566f00122653381227;anchor=swh:1:rev:640e8d6a4813be6b44bee473dfb674f40daac1f0;path=/⟩. ⟨hal-01912024⟩

Accès au texte intégral et bibtex

2017

Journal articles

ref_biblio

Gabriel Braun, Julien Narboux. A synthetic proof of Pappus' theorem in Tarski's geometry. Journal of Automated Reasoning, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩. ⟨hal-01176508v2⟩

Accès au texte intégral et bibtex

2016

Journal articles

ref_biblio

Julien Narboux, David Braun. Towards A Certified Version of the Encyclopedia of Triangle Centers. Mathematics in Computer Science, 2016, 10 (1), pp.17. ⟨10.1007/s11786-016-0254-4⟩. ⟨hal-01174131v2⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

Books

ref_biblio

Julien Narboux, Pascal Schreck, Ileana Streinu (Dir.). Proceedings of ADG 2016. , pp.224, 2016. ⟨hal-01334334⟩

Accès au texte intégral et bibtex

2015

Journal articles

ref_biblio

Sana Stojanovic Durdevic, Julien Narboux, Predrag Janicic. Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry. Annals of Mathematics and Artificial Intelligence, 2015, 73 (3), pp.25. ⟨10.1007/s10472-014-9443-5⟩. ⟨hal-01091011v2⟩

Accès au texte intégral et bibtex

ref_biblio

Michael Beeson, Pierre Boutry, Julien Narboux. Herbrand's theorem and non-Euclidean geometry. Bulletin of Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩. ⟨hal-01071431v3⟩

Accès au texte intégral et bibtex

Preprints, Working Papers, ...

ref_biblio

Pierre Boutry, Julien Narboux, Pascal Schreck. A reflexive tactic for automated generation of proofs of incidence to an affine variety. 2015. ⟨hal-01216750⟩

Accès au texte intégral et bibtex

2014

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

2013

Documents associated with scientific events

ref_biblio

Julien Narboux. Les assistants de preuve, ou comment avoir confiance en ses démonstrations.. Séminaire L, Mar 2013, Strasbourg, France. ⟨hal-00809448⟩

Accès au texte intégral et bibtex

2012

Journal articles

ref_biblio

Nicolas Magaud, Julien Narboux, Pascal Schreck. A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem. Computational Geometry, 2012, Special Issue on geometric reasoning, 45 (8), pp.406-424. ⟨10.1016/j.comgeo.2010.06.004⟩. ⟨inria-00432810v2⟩

Accès au texte intégral et bibtex

ref_biblio

Predrag Janicic, Julien Narboux, Pedro Quaresma. The Area Method : a Recapitulation. Journal of Automated Reasoning, 2012, 48 (4), pp.489-532. ⟨10.1007/s10817-010-9209-7⟩. ⟨hal-00426563v2⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

2011

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

Books

ref_biblio

Julien Narboux, Schreck Pascal, Jürgen Richter-Gebert (Dir.). Automated Deduction in Geometry - 8th International Workshop, Revised Selected Papers. Pascal Schreck and Julien Narboux and Jürgen Richter-Gebert. Springer, 6877, pp.258, 2011, Lecture Notes in Computer Science, 978-3-642-25069-9. ⟨10.1007/978-3-642-25070-5⟩. ⟨hal-00644313⟩

Accès au bibtex

2009

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

2008

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

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⟩

Accès au texte intégral et bibtex

2007

Journal articles

ref_biblio

Julien Narboux. A Graphical User Interface for Formal Proofs in Geometry.. Journal of Automated Reasoning, 2007, Special Issue on User Interfaces in Theorem Proving, 39 (2), pp.161-180. ⟨10.1007/s10817-007-9071-4⟩. ⟨inria-00118903⟩

Accès au texte intégral et bibtex

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

ref_biblio

Julien Narboux. GeoProof: A user interface for formal proofs in geometry. MathUI 07, Jun 2007, Linz, Austria. ⟨inria-00495958⟩

Accès au bibtex

2006

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

Theses

ref_biblio

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

Accès au texte intégral et bibtex

Preprints, Working Papers, ...

ref_biblio

Julien Narboux. A formalization of diagrammatic proofs in abstract rewriting. 2006. ⟨inria-00180065⟩

Accès au texte intégral et bibtex

2005

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex

2004

Conference papers

ref_biblio

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⟩

Accès au texte intégral et bibtex