Nicolas Magaud

ORCID

Publication Activity (10 Years)

Years Active: 2000-2024
Publications (10 Years): 12

Top Venues

CoRR

Ann. Math. Artif. Intell.

ITP

Math. Struct. Comput. Sci.

University of Nice Sophia Antipolis, France (PHD)

Education History

University of Nice Sophia Antipolis, France

PHD

Publications

Nicolas Magaud
Towards Automatic Transformations of Coq Proof Scripts. CoRR (2024)
David Braun, Nicolas Magaud, Pascal Schreck
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry. J. Autom. Reason. 68 (1) (2024)
Catherine Dubois, Nicolas Magaud, Alain Giorgetti
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families. CoRR (2022)
Nicolas Magaud
Spreads and Packings of PG(3, 2), Formally! CoRR (2022)
Pascal Schreck, Nicolas Magaud, David Braun
Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach. CoRR (2022)
Loïc Mazo, Marie-Andrée Jacob-Da Col, Laurent Fuchs, Nicolas Magaud, Gaëlle Skapin
Some representations of real numbers using integer sequences. Math. Struct. Comput. Sci. 32 (5) (2022)
Catherine Dubois, Nicolas Magaud, Alain Giorgetti
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. TYPES (2022)
Nicolas Magaud
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant. ITP (2022)
Nicolas Magaud
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant. PxTP (2021)
David Braun, Nicolas Magaud, Pascal Schreck
Two New Ways to Formally Prove Dandelin-Gallucci's Theorem. ISSAC (2021)
David Braun, Nicolas Magaud, Pascal Schreck
Two cryptomorphic formalizations of projective incidence geometry. Ann. Math. Artif. Intell. 85 (2-4) (2019)
David Braun, Nicolas Magaud, Pascal Schreck
Formalizing Some "Small" Finite Models of Projective Geometry in Coq. AISC (2018)
Nicolas Magaud, Agathe Chollet, Laurent Fuchs
Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. Ann. Math. Artif. Intell. 74 (3-4) (2015)
Nicolas Magaud, Julien Narboux, Pascal Schreck
A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. 45 (8) (2012)
Christophe Brun, Jean-François Dufourd, Nicolas Magaud
Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. Automated Deduction in Geometry (2012)
Christophe Brun, Jean-François Dufourd, Nicolas Magaud
Designing and proving correct a convex hull algorithm with hypermaps in Coq. Comput. Geom. 45 (8) (2012)
Nicolas Magaud, Julien Narboux, Pascal Schreck
Formalizing Desargues' theorem in Coq using ranks. SAC (2009)
Nicolas Magaud, Julien Narboux, Pascal Schreck
Formalizing Projective Plane Geometry in Coq. Automated Deduction in Geometry (2008)
Nicolas Magaud
Changing Data Representation within the Coq System. TPHOLs (2003)
Yves Bertot, Nicolas Magaud, Paul Zimmermann
A Proof of GMP Square Root. J. Autom. Reason. 29 (3-4) (2002)
Nicolas Magaud, Yves Bertot
Changement de représentation des structures de données en Coq: le cas des entiers naturels. JFLA (2001)
Nicolas Magaud, Yves Bertot
Changing Data Structures in Type Theory: A Study of Natural Numbers. TYPES (2000)

Nicolas Magaud.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Nicolas Magaud