Documentation
Français (FR)

Anglais (EN)

Nicolas Magaud

Professeur des Universités en Informatique (Université de Strasbourg)

33

Documents

Publications

	A proof of GMP square root using the Coq assistant Yves Bertot , Nicolas Magaud , Paul Zimmermann [Research Report] RR-4475, INRIA. 2002 Rapport inria-00072113v1
	Changements de représentation des données dans le calcul des constructions inductives Nicolas Magaud , Yves Bertot [Rapport de recherche] RR-4039, INRIA. 2000, pp.29 Rapport inria-00072599v1

	Changements de Représentation des Données dans le Calcul des Constructions Nicolas Magaud Génie logiciel [cs.SE]. Université Nice Sophia Antipolis, 2003. Français. ⟨NNT : ⟩ Thèse tel-00005903v1

	Pragmatic isomorphism proofs between Coq representations: application to lambda-term families Catherine Dubois , Nicolas Magaud , Alain Giorgetti 28th International Conference on Types for Proofs and Programs (TYPES 2022), Nantes, France, Jan 2023, Nantes, France Communication dans un congrès hal-04094291v1
	Towards Automatic Transformations of Coq Proof Scripts Nicolas Magaud 14th International Conference on Automated Deduction in Geometry Belgrade, Serbia, September 20-22, 2023, Nov 2023, Belgrade, Serbia Communication dans un congrès hal-04328058v1
	Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant Nicolas Magaud The International conference Interactive Theorem Proving (ITP) 2022, Jul 2022, Haïfa, Israel. ⟨10.4230/LIPIcs.ITP.2022.25⟩ Communication dans un congrès hal-03633318v1
	Pragmatic isomorphism proofs between coq representations: application to lambda-term families Catherine Dubois , Nicolas Magaud , Alain Giorgetti 28th International Conference on Types for Proofs and Programs (TYPES 2022), Jun 2022, Nantes, France. pp.11:1-11:19, ⟨10.4230/LIPIcs.TYPES.2022.11⟩ Communication dans un congrès hal-04245455v1
	Two New Ways to Formally Prove Dandelin-Gallucci's Theorem David Braun , Nicolas Magaud , Pascal Schreck ISSAC 2021 : International Symposium on Symbolic and Algebraic Computation, Jul 2021, Saint Petersburg (virtual event), Russia. ⟨10.1145/3452143.3465550⟩ Communication dans un congrès hal-03225987v1
	Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant Nicolas Magaud Seventh Workshop on Proof eXchange for Theorem Proving PxTP 2021, Jul 2021, En ligne, France. ⟨10.4204/EPTCS.336.4⟩ Communication dans un congrès hal-03268103v1
	Formalizing Some “Small” Finite Models of Projective Geometry in Coq David Braun , Nicolas Magaud , Pascal Schreck 13th International Conference Artificial Intelligence and Symbolic Computation ( AISC 2018 ), Sep 2018, Suzhou, China. ⟨10.1007/978-3-319-99957-9⟩ Communication dans un congrès hal-03797843v1
	Formalizing Some " Small " Finite Models of Projective Geometry in Coq David Braun , Nicolas Magaud , Pascal Schreck Proceedings of the 13th International Conference on Artificial Intelligence and Symbolic Computation (AISC'2018), Sep 2018, Suzhou, China Communication dans un congrès hal-01835493v1
	Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations Nicolas Magaud CoqPL 2017: The Third International Workshop on Coq for Programming Languages, Jan 2017, Paris, France Communication dans un congrès hal-01518660v1
	Des preuves formelles en Coq du théorème de Thalès pour les cercles David Braun , Nicolas Magaud Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France Communication dans un congrès hal-01099132v1
	Dealing with arithmetic overflows in the polyhedral model Bruno Cuervo Parrino , Julien Narboux , Eric Violard , Nicolas Magaud IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Louis-Noel Pouchet, Jan 2012, Paris, France Communication dans un congrès hal-00655485v1
	Formal Proof in Coq and Derivation of a Program in C++ to Compute Convex Hulls Christophe Brun , Jean-François Dufourd , Nicolas Magaud Automated Deduction in Geometry (Post-proceedings), Sep 2012, Edinbourg, United Kingdom. pp.71-88, ⟨10.1007/978-3-642-40672-0_6⟩ Communication dans un congrès hal-00916880v1
	Formalizing Desargues' theorem in Coq using ranks in Coq Nicolas Magaud , Julien Narboux , Pascal Schreck 24th Annual ACM Symposium on Applied Computing, Xiao-Shan Gao, Robert Joan-Arinyo, Dominique Michelucci, Mar 2009, Honolulu, United States. pp.1110-1115, ⟨10.1145/1529282.1529527⟩ Communication dans un congrès inria-00335719v1
	Formalizing Projective Plane Geometry in Coq Nicolas Magaud , Julien Narboux , Pascal Schreck Post-proceedings of Automated Deduction in Geometry (ADG) 2008, Thomas Sturm, Sep 2008, Shanghai, China. pp.141-162, ⟨10.1007/978-3-642-21046-4⟩ Communication dans un congrès inria-00305998v3

	Actes des Journées Francophones des Langages Applicatifs 2019 Nicolas Magaud , Zaynah Dargaye Université de Strasbourg, 2019 Ouvrages hal-03247238v1
	Actes des Journées Francophones des Langages Applicatifs 2018 Sylvie Boldo , Nicolas Magaud INRIA, 2018 Ouvrages hal-03255943v1

	A Matroid-based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry David Braun , Nicolas Magaud , Pascal Schreck Journal of Automated Reasoning, 2023, in press (1), pp.3. ⟨10.1007/s10817-023-09690-2⟩ Article dans une revue hal-04318847v1
	Some representations of real numbers using integer sequences Loïc Mazo , Marie-Andrée Jacob-da Col , Laurent Fuchs , Nicolas Magaud , Gaëlle Largeteau-Skapin Mathematical Structures in Computer Science, 2022, 32 (5), pp.648-681. ⟨10.1017/S0960129522000342⟩ Article dans une revue hal-03276295v2
	Two Cryptomorphic Formalizations of Projective Incidence Geometry David Braun , Nicolas Magaud , Pascal Schreck Annals of Mathematics and Artificial Intelligence, inPress Article dans une revue hal-01887000v1
	Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective Nicolas Magaud , Agathe Chollet , Laurent Fuchs Annals of Mathematics and Artificial Intelligence, 2015, ⟨10.1007/s10472-014-9434-6⟩ Article dans une revue hal-01066671v1
	A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem Nicolas Magaud , Julien Narboux , Pascal Schreck Computational Geometry, 2012, Special Issue on geometric reasoning, 45 (8), pp.406-424. ⟨10.1016/j.comgeo.2010.06.004⟩ Article dans une revue inria-00432810v2
	Designing and proving correct a convex hull algorithm with hypermaps in Coq Christophe Brun , Jean-François Dufourd , Nicolas Magaud Computational Geometry, 2012, 45 (8), pp.436-457. ⟨10.1016/j.comgeo.2010.06.006⟩ Article dans une revue hal-00955400v1
	A Proof of GMP Square Root Yves Bertot , Nicolas Magaud , Paul Zimmermann Journal of Automated Reasoning, 2002, 29 (3-4), pp.225--252. ⟨10.1023/A:1021987403425⟩ Article dans une revue inria-00101044v1

	Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach Pascal Schreck , Nicolas Magaud , David Braun Automated Deduction in Geometry (ADG 2021), Jan 2021, Hagenberg, Austria. 2021 Poster de conférence hal-03402842v1
	Spreads and Packings of PG(3,2), Formally! Nicolas Magaud Automated Deduction in Geometry (ADG 2021), 2021, Hagenberg, Austria. 2021 Poster de conférence hal-03398276v1

	Contributions au développement des méthodes formelles de preuves et applications à la géométrie Nicolas Magaud Géométrie algorithmique [cs.CG]. Université de Strasbourg, 2020 HDR tel-03229264v1

	Journées Francophones des Langages Applicatifs 2019 Nicolas Magaud , Zaynah Dargaye Nicolas Magaud; Zaynah Dargaye. Journées Francophones des Langages Applicatifs 2019, Jan 2019, Les Rousses, France. publié par les auteurs, 2019 Proceedings/Recueil des communications hal-01985195v1
	Journées Francophones des Langages Applicatifs 2018 Sylvie Boldo , Nicolas Magaud Sylvie Boldo; Nicolas Magaud. Journées Francophones des Langages Applicatifs 2018, Jan 2018, Banyuls-sur-Mer, France. publié par les auteurs, 2018 Proceedings/Recueil des communications hal-01707376v1

	Combinatoire certifiée Alain Giorgietti , Nicolas Magaud GdR Génie de la Programmation et du Logiciel, Défis 2030, pp.61-65, 2021 Chapitre d'ouvrage hal-03417881v1

	Programming with Dependent Types in Coq: a Study of Square Matrices Nicolas Magaud 2004 Pré-publication, Document de travail hal-00955444v1