Me

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.