Me

2024

  • Animation d'un atelier sur l'utilisation des assistants de preuve pour l'enseignement de la démonstration, Doctoriales, Angers
  • Séminaire ITI IRMIA++ Strasbourg (45 minutes talk) (.pdf)
  • Participation à la table ronde sur l'utilisation des assistants de preuve pour l'enseignement. Journées Nationales de l'Informatique Mathématique. Grenoble. (.pdf)

2023

  • Formalisation, arithmetization and automatisation of geometry, invited talk at ADG 2023
  • Underlying theories of proof assistants and potential impact on the teaching and learning of proof at Thedu 2023
  • Tutorial about GeoCoq with Pierre Boutry at ADG 2023

2022

  • GeoCoq library and its porting to Isabelle, joint talk with Roland Coghetto, EUROProofNet Workshop, Sept 2022 [.pdf].
  • Mechanization of geometric reasoning, ITI IRMIA++ Seminar, Oct 2022 [.pdf].

2021

  • Theorem Proving as Constraints Solving, joint work with Predrag Janicic, Dagstuhl, November 2021 [.pdf].

2020

  • Les assistants de preuves, vers une utilisation en classe, Toulouse, Février 2020. [.pdf]

2019

  • Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq, Séminaire Equipe Marelle, INRIA Sophia-Antipolis. [.pdf]

2018

  • Vers l'utilisation d'un assistant de preuve en classe ?, IREM de Strasbourg. [.pdf]
  • ITP for the education and an overview of GeoCoq, TheEDU 2018 Invited Talk, Oxford [.pdf]
  • Mécanisation du raisonnement géométrique, Ecole Thématique MPHC Mathématiques et Philosophie Contemporaines, Saint-Flour, Juin 2018 [.pdf]

2017

  • Formalization of foundations of geometry, from Hilbert and Tarski to Euclid, Argo Group Seminar, Belgrade [.pdf]
  • Les assistants de preuves et applications à l'education, Séminaire de Recherche en Didactique et Epistemologie des Mathématiques de l'Université de Montpellier [.pdf]

2015

  • Toward a Certified Encyclopedia of Geometry, Invited Talk at GC2015 [.pdf]
  • The parallel postulate: a syntactic proof of independence, 15 minutes Talk at IGG seminar [.pdf]

2014

  • Les assistants de preuve ou comment avoir confiance en ses démonstrations, Séminaire IRMA [.pdf]

2012

  • From Tarski to Hilbert, Automated Deduction in Geometry 2012 [.pdf]

2010

  • A presentation of GeoProof, Automated Deduction- Geogebra meeting, Castro Urdiales [.pdf]

2009

  • Formalization of projective geometry in Coq GDR LTP, University Paris XII [.pdf]

2008

  • Vers une preuve du théorème de Pick en Coq, Journées Galapagos, décembre 2008 [.pdf]

2007

  • Formalisation and automation of geometry in Coq. LAMA/Logic-ENS/Plume's seminar, Chambery, March 2007.
  • Proving the prover: Wu's method formalised. LogiCal seminar, INRIA Futurs, March 2007.
  • An introduction to the Nominal Package. LogiCal seminar, INRIA Futurs, March 2007.
  • Nominal Formalisation of Typical SOS Proofs. Gallium-Moscova seminar, INRIA Rocquencourt, February 2007.

2006

  • Formalisation du raisonnement diagrammatique en réécriture et interface graphique. au séminaire de Géométrie Algébrique au laboratoire Dieudonné à Nice, Juin 2006.
  • Formalisation de la géométrie de Tarski, au séminaire de l'équipe Marelle à l'INRIA Sophia Antipolis, Juin 2006. 
  • Formalization and automation of geometric reasoning within the Coq proof assistant, Club2 seminar, TU Munich [.pdf]

2005

2004

  • I have presented a poster at TYPES, December 2004 Poster image
  • A Decision Procedure for Geometry in Coq, TPHOLs 2004, Park City, Utah

2003

  • Automatisation de la géométrie [pdf | html], à la journée Géométrie Formelle à l'ENS-Lyon en Juillet 2003.