(2019) Aspects pratiques de la théorie des types, talk at "Café-In", outreach seminar for Inria employees (sources here)
(2018) Aspects pratiques de la théorie des types talk at Collège de France (sources here, video here, Inria page here)
(2017) Building blocks towards modeling the physical world:analysis, geometry, arithmetic, talk at the Isaac Newton Institute, July 2017.
(2016) The EasyCrypt Family, a very short presentation of work by B. Grégoire and his colleagues.
(2015) Formalized proof of transcendance for π, Workshop on Realistic Program Verification, Nijmegen, December, 2015.
(2015) A general presentation of links with the University of Science and Technology of China, November, 2015.
(2015) A talk on using Bernstein coefficients to prove the positivity of multi-variate polynomials, Lyon, May 2015. Coq files, to be used with coq-8.5beta2
(2015) An introductory presentation of Coq for a technical audience, Sophia Antipolis, May 2015.
(2014) Arithmetic-geomtric means for pi, a formal study and computation inside Coq Special JFLI Seminar on formal proofs in Coq, Tokyo, August 2014.
(2014) A naive view of Homotopy Type Theory and its relation to the Calculus of Constructions (CICM 2014 invited conference), Coimbra, Portugal, July 2014.
(2014) PI, Arithmetic geometric means, and formal verification in Coq using Coquelicot Mathematical Structures of Computation, Lyon, February 2014.
(2011) A tutorial on co-induction at JFLA-11 and the associated Coq file.
A talk on general co-recursion, Paris, november 2010. the associated Coq file.