Nicolas Magaud Professeur des Universités - Université de Strasbourg Recherche : Enseignement : Equipe Informatique Géométrique et Graphique Département d'Informatique Icube, UMR 7357 CNRS-Université de Strasbourg UFR Mathématique - Informatique Pôle API - 300 Boulevard Sébastien Brant - CS 10413        7, rue René Descartes 67412 Illkirch Cedex - FRANCE 67084 Strasbourg Cedex - FRANCE Pôle API: Bureau C109 - Tel: (+33) 3 68 85 44 66 Esplanade: Bureau 302 - Tel: (+33) 3 68 85 02 46 Fax: (+33) 3 68 85 44 55 (Pôle API) Fax : (+33) 3 68 85 03 29 (Esplanade) Courriels/E-mails:magaud @ unistra.fr, nicolas.magaud @ ens-lyon.org

Recent and upcoming events

• Offre de thèse 2025 :

  • Formalisation en Coq de la complétude des axiomes de Tarski pour la géométrie euclidienne. Thèse co-encadrée avec Pierre Boutry.
    Possibilité de bourse de l'école doctorale Mathématiques, Sciences de l'Information et de l'Ingénieur (MSII), sur sélection (me contacter pour postuler).

• M2 / final year internships (spring 2026) :

  • Source-to-source Transformations of Coq/Rocq Proof Scripts: Removing, Inlining, Expanding Tactics
  • A formal study of finite projective planes using Rocq
  • Automatic proofs in projective geometry : finite projective spaces, spreads, and packings

• Organisateur de la journée annuelle (13 novembre 2025) du groupe Langages et Vérification de Programmes (LVP) du GDR GPL

• Co-organizer of the summer school "Deep Learning and applications"(Aug 25 – 29, 2025 - ITI IRMIA++, Strasbourg, France)

• Organisateur des journées nationales du GDR GPL 2024, avec Arthur Charguéraud et Julien Narboux.

• Co-responsable du GT Languages, Vérification et Preuves (LVP) du GDR Génie de la Programmation et du Logiciel (GPL) (depuis mai 2023)

• International workshop talk at ADG 2023 (Automated Deduction in Geometry) in Belgrade, Serbia (proceedings paper)

• Co-organizer and lecturer at the PAT 2023 Thematic School Proof assistants for teaching proof and proving, 19 - 23 June 2023, Val d'Ajol, France

• Workshop talk at CLA 2023 (Computational Logic and Applications) at Ecole Polytechnique, France

• European Research Network on Formal Proofs EuroProofNet (formal information by COST association), October 11, 2021 - October 10, 2025 (action chair: Frédéric Blanqui, action vice chair: Sandra Alves).

  I am a member of the working groups WG1 (Tools for interoperability of proof systems), WG2 (Automated theorem provers) and WG4 (Libraries of formal proofs).

• New conference paper published: Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant (slides of the talk given at ITP 2022, Haifa, Israel)

• Expert HCERES 2024

• Expert Crédit Impôt Recherche pour le Ministère de l'Enseignement Supérieur et de la Recherche

• Organisateur des sessions "Posters et Démos" pour les journées nationales du GDR GPL 2022 et la conférence AFADL 2022 (7-10 juin 2022 - Vannes, France), et pour les journées nationales du GDR GPL 2023 et la conférence AFADL 2023 (5-9 juin 2023 - Rennes, France)
• Membre élu du CNU27 (juin 2022-novembre 2023)
• Starting Jan. 2022: Co-organizer of the interdisciplinary seminar of the ITI Research in Mathematics, Interactions & Applications (IRMIA++) (with Alexandru Oancea and Benoît Famaey)
• Soutenance d'habilitation à diriger des recherches le vendredi 06 novembre 2020.
• Ecole de Jeunes Chercheurs en Programmation (EJCP 2019) du GDR GPL, Strasbourg, 24-28 juin 2019.
• Journées Francophones des Langages Applicatifs (JFLA 2019), Les Rousses, 30 janvier - 2 février 2019 (actes).
• Journées Francophones des Langages Applicatifs (JFLA 2018), Banyuls-sur-mer, 24-27 janvier 2018 (actes).
• The Coq workshop 2016, in Nancy, France (August 26 2016): a satellite workshop of ITP 2016.
• ADG 2016: the next workshop of Automated Deduction in Geometry will be held in Strasbourg , France (June 27-29 2016).

Internships / offres de stages et de thèse

• Offre de thèse 2024 :

  • Automatisation, maintenance et réutilisation des démonstrations dans l’assistant de preuves Coq : applications aux mathématiques et à la géométrie.
    Possibilité de bourse de l'école doctorale Mathématiques, Sciences de l'Information et de l'Ingénieur (MSII), sur sélection (me contacter pour postuler).

• Offre(s) de stage de master pour le printemps 2023 (M2 ou École d'ingénieurs)

  • Portabilité des preuves formelles : traduction automatique de la bibliothèque Geocoq vers Lean (Interoperability of Proof Systems : Translating the GeoCoq Library into Lean), co-supervised with Julien Narboux

  • Robustesse et Maintenance des preuves formelles écrites en Coq (Making Coq Proofs More Reliable and More Easily Reusable)

  • Implantation fonctionnelle d'algorithmes géométriques en 3D (Functional Implementation of Geometric Algorithms in 3D)

  • Géométrie projective et espaces projectifs finis

• Anciens sujets de stages et de thèses

  • Sujet de thèse 2022: Intégration d’outils de preuves automatiques à Coq et applications à la géométrie
  • Etude et formalisation en Coq de la norme ISO8601
  • Géométrie projective et espaces projectifs finis
  • Le problème de l'aiguille de Buffon : étude et formalisation en Coq
  • Transformation affine d’image avec précision arbitraire (en collaboration avec Loïc Mazo et Marie-Andrée Jacob-Da Col)
    
  • D'autres sujets encore plus anciens...

Research Activities

• Fields of research: Type Theory, Data Representations and Proof Transformations, Formal Proofs in Geometry, Proof engineering, Exact Real Computations (using the Harthong-Reeb line)

• Official list of publications (from the Icube lab database)

• Older publications (before 2015)

• Encadrement de thèse 2024-2027 (Alexandre Jean)
  • Du génie logiciel au génie de la preuve

• Encadrement de thèse 2015-2019 (David Braun)
  • Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective (thèse co-encadrée avec Pascal Schreck, soutenue le 23/09/2019, manuscript)

• Recent proof developments in Coq
  • Formalizing a Discrete Model of the Continuum in Coq - the Harthong-Reeb line (joint work with Laurent Fuchs and Agathe Chollet)
  • Des preuves en Coq du théorème de Thalès pour les cercles (travail réalisé avec David Braun)

• TrADiCont : projet interne Icube (2014-2015)

• ANR Project Galapagos: Géométrie, Algorithmes et Preuves (dec. 2007 - oct. 2011)
  • Co-encadrement de la thèse de Christophe Brun dirigée par Jean-François Dufourd (2007-2010, thèse soutenue le 06/12/2010, manuscript)
  • Responsable scientifique local pour le site de Strasbourg
  • Coordinateur des réunions des opérations 2 et 3 (spécifications, contraintes et preuves) de l'équipe IGG (sept. 2007- sept. 2011)

• Program Committees: Journées francophones des langages applicatifs (JFLA'08), Best Paper AFIG/EGFR2014, The Coq workshop 2016 (co-chair), Journées francophones des langages applicatifs 2018 (vice-président), Journées francophones des langages applicatifs 2019 (président)

• Organizer for ADG 2016, The Coq workshop 2016, Journées francophones des langages applicatifs 2018, Journées francophones des langages applicatifs 2019, Ecole de Jeunes Chercheurs en Programmation (EJCP 2019)

• Reviewer for conferences : FLOPS'2006, SAC'2007 (GCR track), JFLA'2008, JFLA'2012, Best Paper AFIG/EGFR2014, SCSS'2016, ITP'2017, JFLA'2018, JFLA'2019, IJCAR'2020, LFMTP'2020, LFMTP'2021.
• Reviewer for international journals : Fundamenta Informaticae, Journal of Automated Reasoning, Computational Geometry: Theory and Applications, Annals of Mathematics and Artificial Intelligence, Journal of Symbolic Computation, Logical Methods in Computer Science

• Some resources related to Coq

Activités d'Enseignement (Teaching)

• CRCT en 2025-2026

• Page dédiée au DUI-EIL 2019

• Délégation CNRS en 2016-2017

• M1-Informatique (+ ENSIIE) : Sémantique des langages de programmation 2014-2016
• L3-Math: Algorithmique et Structure de Données 2006-2016
• DUT Informatique (S3) : Comprendre les systèmes d'exploitation (TDs et TPs) 2014-2016
• DUT Informatique (S2) : Architecture (TDs et TPs) 2015-2016
• L2-Info : PPP (Projet Professionnel Personnalisé : Choisir - Valoriser) 2008-2016

• ENSIIE Strasbourg (1A) : IPF : Introduction à la programmation fonctionnelle 2009-2015
• CNAM Alsace ITII (1A) : Algorithmique 2009-2016

• ENSIIE Strasbourg (2A) : Validation et Vérification du Logiciel (partie : Logique de Hoare et Frama-C) 2009-2012
• M2-ISI / M2-SE : Preuve et certification logicielle - 2007-2012
• M1-Info (+ ENSIIE) : Ingénierie de la Preuve - 2005-2014
• M1-Informatique : Sémantique des langages de programmation - 2005-2010
• M1-ChemoInformatique : Génie logiciel - 2008-2012
• L2-Info : Pratique des systèmes d'exploitation (cours + Tps) - 2012-2014
• L2-Info : Structures de données et algorithmes 2 - 2005-2014
• L2-Info : Structures de données et Algorithmes 1 - 2005-2007
• L1-MathInfo : PPP (Projet professionnel personnalisé) - 2005-2012
• L1-Info : MTU (Méthodologie du Travail Universtaire) - 2012-2013

Responsabilités collectives

• Président de la commission pédagogique de l'UFR Mathématique-Informatique de l'Université de Strasbourg (2015-2025)

• Responsable du parcours SIL (Science et Ingénierie du Logiciel) du Master Informatique de l'Université de Strasbourg (2018-2025)

• Membre du comité d'experts Informatique CE27 de l'Université de Strasbourg (depuis 2024)

• Co-responsable du Master Informatique, spécialité ILC : Ingénierie des Logiciels et des Connaissances (2012-2016)
  • Emplois du temps et relations avec les intervenants extérieurs (issus du monde de l'industrie)
  • Suivi des étudiants apprentis (ou bien stagiaires) et relations avec les entreprises
  • Sélection des étudiants via la commission pédagogique
  • Mise en œuvre de la convention avec l'ENSIIE Strasbourg pour le double diplôme Ingénieur ENSIIE Strasbourg et Master d'Informatique
• Vice-président de la commission pédagogique de l'UFR Mathématique-Informatique de l'Université de Strasbourg (2014-2015)
• Mobilité étudiante internationale : quelques pointeurs pour les étudiants souhaitant partir en échanges internationaux
• Membre du comité d'experts Informatique CE27 de l'Université de Strasbourg (2014-2019)
• Représentant de l'équipe IGG au conseil du DIR : Département Informatique Recherche (2012-2015)
• Correspondant de la Direction des Relations Internationales de l'Université de Strasbourg pour le Département d'Informatique (2009-2016)

• Participation aux similations d'entretiens d'embauche à destination des étudiants - prêt pour l'emploi - (2011-2016)
• Coordinateur pour les enseignements d'APE (APE1 en L1-mathinfo, APE2 en L2-info) pour le département d'Informatique (2011-2015)
• Coordinateur des interventions de l'ULP puis de l'Université de Strasbourg dans les lycées d'Alsace pour le département d'informatique (2006-2010)

Divers

• Vulgarisation : Un aspect de l'ingénierie et du logiciel : la fiabilité du logiciel (journées des Universités - 8 mars 2008)
• Trimester Proofs IHP (youtube channel)

• Président de l'association ASCPA (depuis 2014)
• Vice-président de l'association ASCPA, en charge de la section escalade (2008-2014)
• Trésorier de la Ligue Grand Est FFME (2017-2024)
• Président du Comité départemental 67 de la FFME (2009-2013), membre élu du Comité Régional Alsace de la FFME (2009-2017)
• Initiateur Escalade FFME (2009), arbitre régional Escalade FFME - Président de Jury de niveau 1 (2011), titulaire du PSC1 (2009).

• Quelques résultats en (ultra-)trails

• Scuba diving: CMAS ***, PADI Rescue+Deep+Nitrox.
• North West Island (2 weeks there in Dec. 04 with the UNSW Underwater club).
• Changer d'approche