(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.

Last modified: July 2017