Mots-clés

Nombre de documents

32

Julien Narboux


Article dans une revue7 documents

Communication dans un congrès19 documents

  • Pierre Boutry, Gabriel Braun, Julien Narboux. From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry. James H. Davenport and Fadoua Ghourabi. SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan. EasyChair, 39 (14-28), pp.15, 2016, EPiC Series in Computing. <http://easychair.org/publications/paper/From_Tarski_to_Descartes_Formalization_of_the_Arithmetization_of_Euclidean_Geometry>. <hal-01282550>
  • Gabriel Braun, Pierre Boutry, Julien Narboux. From Hilbert to Tarski. Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19, 2016, Proceedings of ADG 2016. <http://icube-web.unistra.fr/adg2016/index.php/Accueil>. <hal-01332044>
  • 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), Jan 2016, Saint Malo, France. pp.15, 2016, Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016). <http://jfla.inria.fr/2016/>. <hal-01228612v2>
  • Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. A short note about case distinctions in Tarski's geometry. Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15, 2014, Proceedings of ADG 2014. <hal-00989785v2>
  • Sana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic. A Vernacular for Coherent Logic. CICM 2014 - Conferences on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. Springer, 8543, 2014, Lecture Notes in Computer Science. <hal-00983975v2>
  • Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. Using small scale automation to improve both accessibility and readability of formal proofs in geometry. Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-19, 2014, Proceedings of ADG 2014. <hal-00989781v2>
  • Bruno Cuervo Parrino, Julien Narboux, Eric Violard, Nicolas Magaud. Dealing with arithmetic overflows in the polyhedral model. Uday Bondhugula and Vincent Loechner. IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Jan 2012, Paris, France. 2012. <hal-00655485>
  • Gabriel Braun, Julien Narboux. From Tarski to Hilbert. Tetsuo Ida and Jacques Fleuriot. Automated Deduction in Geometry 2012, Sep 2012, Edinburgh, United Kingdom. Springer, 7993, pp.89-109, 2012, <10.1007/978-3-642-40672-0_7>. <hal-00727117v2>
  • 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. IEEE, pp.1139 - 1144, 2012, ICTAI. <10.1109/ICTAI.2012.162>. <hal-00753551>
  • 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. Springer-Verlag, 6785, pp.368-383, 2011, Lecture Notes in Computer Science. <10.1007/978-3-642-21898-9_32>. <inria-00584918>
  • Jean-David Génevaux, Julien Narboux, Pascal Schreck. Formalization of Wu's simple method in Coq. Jean-Pierre Jouannaud and Zhong Shao. CPP 2011 First International Conference on Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. Springer-Verlag, 7086, pp.71-86, 2011, Lecture Notes in Computer Science. <10.1007/978-3-642-25379-9_8>. <inria-00618745v2>
  • Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Desargues' theorem in Coq using ranks in Coq. 24th Annual ACM Symposium on Applied Computing, Mar 2009, Honolulu, United States. ACM, pp.1110-1115, 2009, Proceedings of SAC 2009. <10.1145/1529282.1529527>. <inria-00335719>
  • Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Projective Plane Geometry in Coq. Thomas Sturm. Post-proceedings of Automated Deduction in Geometry (ADG) 2008, Sep 2008, Shanghai, China. Springer, 6301, pp.141-162, 2011, LNAI; Automated Deduction in Geometry. <10.1007/978-3-642-21046-4>. <inria-00305998v3>
  • Christian Urban, Julien Narboux. Formal SOS-Proofs for the Lambda-Calculus. Third Workshop on Logical and Semantic Frameworks, with Applications, Aug 2008, Salvador, Brazil. Elsevier, 247, pp.139-155, 2009, ENTCS; Proceedings of the Third Workshop on Logical and Semantic Frameworks with Applications. <10.1016/j.entcs.2009.07.053>. <inria-00335718>
  • Julien Narboux. GeoProof: A user interface for formal proofs in geometry. MathUI 07, Jun 2007, Linz, Austria. 2007. <inria-00495958>
  • Julien Narboux, Christian Urban. Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.. Brigitte Pientka and Carsten Schürmann. LFMTP'07, Jul 2007, Bremen, Germany. Elsevier, 196, 15p., 2008, ENTCS; Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007). <10.1016/j.entcs.2007.09.014>. <inria-00180061v2>
  • Julien Narboux. Mechanical Theorem Proving in Tarski's geometry.. Eugenio Roanes Lozano, Francisco Botana. Automated Deduction in Geometry 2006, Aug 2006, Pontevedra, Spain. Springer, 4869, pp.139-156, 2007, LNCS; Automated Deduction in Geometry. <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. 2005. <inria-00495952>
  • Julien Narboux. A Decision Procedure for Geometry in Coq. Slind, Konrad; Bunker, Annette; Gopalakrishnan, Ganesh C. Theorem Proving in Higher Order Logics 2004, Jul 2004, Park City, USA, United States. Springer, Lecture Notes In Computer Science, 3223, pp.225-240, 2004, <10.1007/b100400>. <inria-00001035>

Direction d'ouvrage, Proceedings2 documents

  • Julien Narboux, Schreck Pascal, Ileana Streinu. Proceedings of ADG 2016: Eleventh International Workshop on Automated Deduction in Geometry. Jun 2016, Strasbourg, France. pp.224, 2016, <http://icube-web.unistra.fr/adg2016/index.php/Accueil>. <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>

Pré-publication, Document de travail3 documents

  • Pierre Boutry, Julien Narboux, Pascal Schreck. Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski's system of geometry. 2015. <hal-01178236>
  • 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>

Thèse1 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>