Nicolas Magaud

Available identifiers

Publication	Date of Publication	Type
Two new ways to formally prove Dandelin-Gallucci's theorem	2025-01-20	Paper
Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach	2024-12-17	Paper
Spreads and packings of PG(3,2), formally!	2024-12-17	Paper
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families	2024-11-26	Paper
Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant	2024-07-15	Paper
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry	2024-04-29	Paper
Formalizing Some “Small” Finite Models of Projective Geometry in Coq	2023-06-30	Paper
Some representations of real numbers using integer sequences	2023-02-10	Paper
Two cryptomorphic formalizations of projective incidence geometry	2019-05-16	Paper
Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective	2015-07-27	Paper
Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls	2013-09-20	Paper
Designing and proving correct a convex hull algorithm with hypermaps in Coq	2012-09-11	Paper
A case study in formalizing projective geometry in Coq: Desargues theorem	2012-09-11	Paper
Formalizing Projective Plane Geometry in Coq	2011-05-26	Paper
Changing Data Representation within the Coq System	2010-05-07	Paper
https://portal.mardi4nfdi.de/entity/Q4736398	2004-08-09	Paper
A proof of GMP square root	2003-04-27	Paper

This page was built for person: Nicolas Magaud