default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJulien Narboux
Person information
- affiliation: Université Paris Cité, France
- affiliation (former): University of Strasbourg, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
Books and Theses
- 2006
[b1]Julien Narboux:
Formalisation et automatisation du raisonnement géométrique en Coq. (Formalisation and automation of geometric reasoning within Coq). University of Paris-Sud, Orsay, France, 2006
Journal Articles
- 2023
- [j12]Predrag Janicic
, Julien Narboux:
Automated generation of illustrated proofs in geometry and beyond. Ann. Math. Artif. Intell. 91(6): 797-820 (2023) - 2022
- [j11]Predrag Janicic, Julien Narboux:
Theorem Proving as Constraint Solving with Coherent Logic. J. Autom. Reason. 66(4): 689-746 (2022) - 2019
- [j10]Michael Beeson, Julien Narboux, Freek Wiedijk:
Proof-checking Euclid. Ann. Math. Artif. Intell. 85(2-4): 213-257 (2019) - [j9]Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck:
Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq. J. Autom. Reason. 62(1): 1-68 (2019) - [j8]Pierre Boutry, Gabriel Braun, Julien Narboux:
Formalization of the arithmetization of Euclidean plane geometry and applications. J. Symb. Comput. 90: 149-168 (2019) - 2017
- [j7]Gabriel Braun, Julien Narboux:
A Synthetic Proof of Pappus' Theorem in Tarski's Geometry. J. Autom. Reason. 58(2): 209-230 (2017) - 2016
- [j6]Julien Narboux, David Braun:
Towards a Certified Version of the Encyclopedia of Triangle Centers. Math. Comput. Sci. 10(1): 57-73 (2016) - 2015
- [j5]Sana Stojanovic Durdevic, Julien Narboux, Predrag Janicic:
Automated generation of machine verifiable and readable proofs: A case study of Tarski's geometry. Ann. Math. Artif. Intell. 74(3-4): 249-269 (2015) - [j4]Michael Beeson, Pierre Boutry, Julien Narboux:
Herbrand's Theorem and non-Euclidean Geometry. Bull. Symb. Log. 21(2): 111-122 (2015) - 2012
- [j3]Nicolas Magaud, Julien Narboux, Pascal Schreck:
A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. 45(8): 406-424 (2012) - [j2]Predrag Janicic, Julien Narboux, Pedro Quaresma:
The Area Method - A Recapitulation. J. Autom. Reason. 48(4): 489-532 (2012) - 2007
- [j1]Julien Narboux:
A Graphical User Interface for Formal Proofs in Geometry. J. Autom. Reason. 39(2): 161-180 (2007)
Conference and Workshop Papers
- 2025
- [c17]Frédéric Tran Minh, Laure Gonnord, Julien Narboux:
A Lean-based Language for Teaching Proof in High School. CICM 2025: 447-467 - 2024
- [c16]Frédéric Tran Minh, Laure Gonnord, Julien Narboux:
Proof Assistants for Teaching: a Survey. ThEdu@CADE 2024: 1-27 - 2023
- [c15]Salwa Tabet Gonzalez, Predrag Janicic, Julien Narboux:
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving. ADG 2023: 21-37 - 2021
- [c14]Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar:
Semantic parsing of geometry statements using supervised machine learning on synthetic data. CICM Workshops 2021 - [c13]Predrag Janicic, Julien Narboux:
Automated Generation of Illustrations for Synthetic Geometry Proofs. ADG 2021: 91-102 - 2016
- [c12]Pierre Boutry, Gabriel Braun, Julien Narboux:
From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry. SCSS 2016: 14-28 - 2014
- [c11]Sana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic:
A Vernacular for Coherent Logic. CICM 2014: 388-403 - 2012
- [c10]Gabriel Braun, Julien Narboux:
From Tarski to Hilbert. Automated Deduction in Geometry 2012: 89-109 - [c9]Pascal Schreck, Pascal Mathis, Julien Narboux:
Geometric Construction Problem Solving in Computer-Aided Learning. ICTAI 2012: 1139-1144 - 2011
- [c8]Jean-David Génevaux, Julien Narboux, Pascal Schreck:
Formalization of Wu's Simple Method in Coq. CPP 2011: 71-86 - [c7]Tuan-Minh Pham, Yves Bertot, Julien Narboux:
A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. ICCSA (4) 2011: 368-383 - 2009
- [c6]Nicolas Magaud, Julien Narboux, Pascal Schreck:
Formalizing Desargues' theorem in Coq using ranks. SAC 2009: 1110-1115 - 2008
- [c5]Nicolas Magaud, Julien Narboux, Pascal Schreck:
Formalizing Projective Plane Geometry in Coq. Automated Deduction in Geometry 2008: 141-162 - [c4]Christian Urban, Julien Narboux:
Formal SOS-Proofs for the Lambda-Calculus. LSFA 2008: 139-155 - 2007
- [c3]Julien Narboux, Christian Urban:
Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. LFMTP@CADE 2007: 3-18 - 2006
- [c2]Julien Narboux:
Mechanical Theorem Proving in Tarski's Geometry. Automated Deduction in Geometry 2006: 139-156 - 2004
- [c1]Julien Narboux:
A Decision Procedure for Geometry in Coq. TPHOLs 2004: 225-240
Editorship
- 2025
- [e3]Julien Narboux, Walther Neuper, Pedro Quaresma:
Proceedings The 13th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2024, Nancy, France, 1-2nd July 2024. EPTCS 419, 2025 [contents] - 2024
- [e2]Julien Narboux, Walther Neuper, Pedro Quaresma:
Proceedings 12th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2023, Rome, Italy, 5th July 2023. EPTCS 400, 2024 [contents] - 2011
- [e1]Pascal Schreck, Julien Narboux, Jürgen Richter-Gebert:
Automated Deduction in Geometry - 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers. Lecture Notes in Computer Science 6877, Springer 2011, ISBN 978-3-642-25069-9 [contents]
Informal and Other Publications
- 2017
- [i2]Michael Beeson, Julien Narboux, Freek Wiedijk:
Proof-checking Euclid. CoRR abs/1710.00787 (2017) - 2014
- [i1]Sana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic:
A Vernacular for Coherent Logic. CoRR abs/1405.3391 (2014)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2026-05-04 23:41 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
