Nicolas Magaud

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

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 Journal of Automated Reasoning	2024-04-29	Paper
Formalizing Some “Small” Finite Models of Projective Geometry in Coq Artificial Intelligence and Symbolic Computation	2023-06-30	Paper
Some representations of real numbers using integer sequences Mathematical Structures in Computer Science	2023-02-10	Paper
Two cryptomorphic formalizations of projective incidence geometry Annals of Mathematics and Artificial Intelligence	2019-05-16	Paper
Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective Annals of Mathematics and Artificial Intelligence	2015-07-27	Paper
Formal proof in Coq and derivation of an imperative program to compute convex hulls Automated Deduction in Geometry	2013-09-20	Paper
Designing and proving correct a convex hull algorithm with hypermaps in Coq Computational Geometry	2012-09-11	Paper
A case study in formalizing projective geometry in Coq: Desargues theorem Computational Geometry	2012-09-11	Paper
Formalizing projective plane geometry in Coq Automated Deduction in Geometry	2011-05-26	Paper
Changing data representation within the \textsf{Coq} system Lecture Notes in Computer Science	2010-05-07	Paper
scientific article; zbMATH DE number 2085174 (Why is no real title available?)	2004-08-09	Paper
A proof of GMP square root Journal of Automated Reasoning	2003-04-27	Paper

Research outcomes over time

This page was built for person: Nicolas Magaud