Nicolas Magaud

Nicolas Magaud is a Professor at the Université de Strasbourg, affiliated with the Département d'Informatique within the UFR Mathématique-Informatique. He leads research in formal proofs, type theory, and discrete geometry, focusing on applications in Coq proof assistant development. His work includes formalizing geometric theorems, automated proof techniques, and discrete models of real numbers like the Harthong-Reeb line. He has organized national conferences such as the GDR GPL 2024 and co-chaired the EuroProofNet COST action. Magaud has supervised multiple PhD students, including Alexandre Jean and David Braun, and contributed to projects like Galapagos (geometric algorithms and proofs).

Research Interests: His primary areas are formal methods, proof engineering, and computational geometry. He develops tools for proof automation in geometry and explores certified combinatorial approaches. Recent work includes formalizing spreads/packings in projective spaces and integrating automated provers into Coq.

Publications: Over 20 peer-reviewed articles, emphasizing formal proof development in geometry and type theory. Notable contributions include mechanizing projective geometry in Coq, formalizing Thales' theorem, and verifying GMP's square root algorithm. Recent focus areas include matroid-based provers and discrete real number representations.

Grants & Administration: Co-leads the ICube Lab's research projects and serves on committees for the GDR GPL and HCERES. He was elected to the CNU27 (National University Council) and chairs the Master's program in Software Engineering. Magaud also coordinates interdisciplinary seminars and teaches advanced courses on proof systems and formal verification.