Mots-clés

Nombre de documents

34

Julien Narboux


Article dans une revue9 documents

Communication dans un congrès19 documents

  • 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〉
  • 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〉
  • 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〉
  • 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, pp.16, 2014, Lecture Notes in Computer Science. 〈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. Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15, 2014, Proceedings of ADG 2014. 〈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. 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. 〈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. 〈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. 〈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. 〈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, Proceedings, Dossier2 documents

Pré-publication, Document de travail3 documents

  • Michael Beeson, Julien Narboux, Freek Wiedijk. Proof-checking Euclid. 2017. 〈hal-01612807〉
  • 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〉