Folgen
Nicolas Magaud
Nicolas Magaud
Associate Professor, University of Strasbourg
Bestätigte E-Mail-Adresse bei unistra.fr - Startseite
Titel
Zitiert von
Zitiert von
Jahr
A proof of GMP square root
Y Bertot, N Magaud, P Zimmermann
Journal of Automated Reasoning 29 (3-4), 225-252, 2002
502002
Changing data representation within the Coq system
N Magaud
TPHOLs 2758, 87-102, 2003
412003
Formalizing projective plane geometry in Coq
N Magaud, J Narboux, P Schreck
Automated Deduction in Geometry: 7th International Workshop, ADG 2008 …, 2011
362011
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
322012
Changing data structures in type theory: A study of natural numbers
N Magaud, Y Bertot
Types for Proofs and Programs: International Workshop, TYPES 2000 Durham, UK …, 2002
302002
Certification of sorting algorithms in the system Coq
JC Filliâtre, N Magaud
Theorem Proving in Higher Order Logics: Emerging Trends, 1999
281999
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
272009
A case study in formalizing projective geometry in Coq: Desargues theorem
N Magaud, J Narboux, P Schreck
Computational Geometry 45 (8), 406-424, 2012
252012
Certification of sorting algorithms in the Coq system
JC Filliâtre, N Magaud
141999
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
122015
Formalizing some “small” finite models of projective geometry in Coq
D Braun, N Magaud, P Schreck
Artificial Intelligence and Symbolic Computation: 13th International …, 2018
102018
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
92001
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
82016
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
72012
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
62015
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
62013
Two cryptomorphic formalizations of projective incidence geometry
D Braun, N Magaud, P Schreck
Annals of Mathematics and Artificial Intelligence 85, 193-212, 2019
52019
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
52010
Changements de Représentation des Données dans le Calcul des Constructions
N Magaud
Université Nice Sophia Antipolis, 2003
52003
Programming with dependent types in coq: a study of square matrices
N Magaud
32004
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20