Nicolas Magaud

24 papers B 2Misc 2Journal 8Unranked 10

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