2024
- Using a proof assistant in an
introduction to proof course: first experiment with two
proof assistants talk given at ThEdu 2024 by Iro Bartzia
.pdf
- 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
- Tutorial
Coq [.pdf],
présenté à ICTMT7 (7th International
Conference on Technology in Mathematics Teaching), Bristol,
Grand-Bretagne, Juillet 2005
- Generic
Sketches, Using
a GUI
for interactive proof in geometry,
ENS-Lyon, Juin 2005
- When a GUI
for dynamic
geometry becomes an interactive
proof language [.pdf],
High
Level Languages for Proofs Workshop, Chambery,
Avril
2005
- Automation
of Geometry using Coq, Cisa
seminar, Edimbourg, Mars 2005
2004
- I have presented a poster at TYPES, December 2004
- 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.
