| A proof of GMP square root Y Bertot, N Magaud, P Zimmermann Journal of Automated Reasoning 29 (3), 225-252, 2002 | 51 | 2002 |
| Changing data representation within the Coq system N Magaud Theorem Proving in Higher Order Logics: 16th International Conference …, 2003 | 43 | 2003 |
| Formalizing projective plane geometry in Coq N Magaud, J Narboux, P Schreck Automated Deduction in Geometry: 7th International Workshop, ADG 2008 …, 2011 | 38 | 2011 |
| Designing and proving correct a convex hull algorithm with hypermaps in Coq C Brun, JF Dufourd, N Magaud Computational Geometry 45 (8), 436-457, 2012 | 34 | 2012 |
| Changing data structures in type theory: A study of natural numbers N Magaud, Y Bertot International Workshop on Types for Proofs and Programs, 181-196, 2000 | 31 | 2000 |
| Formalizing Desargues' theorem in Coq using ranks N Magaud, J Narboux, P Schreck Proceedings of the 2009 ACM symposium on applied computing, 1110-1115, 2009 | 29 | 2009 |
| Certification of sorting algorithms in the system Coq JC Filliâtre, N Magaud Theorem Proving in Higher Order Logics: Emerging Trends, 1999 | 29 | 1999 |
| A case study in formalizing projective geometry in Coq: Desargues theorem N Magaud, J Narboux, P Schreck Computational Geometry 45 (8), 406-424, 2012 | 26 | 2012 |
| Certification of sorting algorithms in the Coq system JC Filliâtre, N Magaud Theorem Proving in Higher Order Logics: Emerging Trends, 1999 | 19 | 1999 |
| Formalizing some “small” finite models of projective geometry in Coq D Braun, N Magaud, P Schreck Artificial Intelligence and Symbolic Computation: 13th International …, 2018 | 13 | 2018 |
| Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective N Magaud, A Chollet, L Fuchs Annals of Mathematics and Artificial Intelligence 74, 309-332, 2015 | 12 | 2015 |
| An equivalence proof between rank theory and incidence projective geometry D Braun, N Magaud, P Schreck Proceedings of automated deduction in geometry, 62-77, 2016 | 8 | 2016 |
| Changements de repr sentation des structures de donn es dans Coq: le cas des entiers naturels N Magaud, Y Bertot Proceedings of JFLA 1, 2001 | 8 | 2001 |
| Two cryptomorphic formalizations of projective incidence geometry D Braun, N Magaud, P Schreck Annals of Mathematics and Artificial Intelligence 85, 193-212, 2019 | 6 | 2019 |
| Des preuves formelles en Coq du théorème de Thalès pour les cercles D Braun, N Magaud Vingt-sixiemes Journées Francophones des Langages Applicatifs (JFLA 2015), 2015 | 6 | 2015 |
| Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls C Brun, JF Dufourd, N Magaud Automated Deduction in Geometry: 9th International Workshop, ADG 2012 …, 2013 | 6 | 2013 |
| Two New Ways to Formally Prove Dandelin-Gallucci's Theorem D Braun, N Magaud, P Schreck Proceedings of the 2021 on International Symposium on Symbolic and Algebraic …, 2021 | 5 | 2021 |
| Dealing with arithmetic overflows in the polyhedral model BC Parrino, J Narboux, E Violard, N Magaud IMPACT 2012-2nd International Workshop on Polyhedral Compilation Techniques, 2012 | 5 | 2012 |
| Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective N Magaud, A Chollet, L Fuchs Automated Deduction in Geometry, ADG 10, 22-24, 2010 | 5 | 2010 |
| Changements de Représentation des Données dans le Calcul des Constructions N Magaud Université Nice Sophia Antipolis, 2003 | 5 | 2003 |
Pascal Schreckprofesseur d'informatique, Université de Strasbourg在 unistra.fr 的电子邮件经过验证
