Talks

2015
Towards verified computer algebra. Inria Saclay - Île de France, January 26, Saclay, France View slides (pdf)
Coqonut: a formally verified JIT compiler for Coq. PPS lab, January 7, Paris, France View slides (pdf)
2014
Parametricity and refinements for effective algebra in Coq. MIT CSAIL, April 8, Boston, USA
Termination and type isomorphisms. Inria Paris-Rocquencourt, February 14, Paris, France View slides (pdf)
Parametricity and refinements for effective algebra in Coq. PPS lab, February 13, Paris, France View slides (pdf)
2013
Towards primitive data types for Coq: 63-bits integers and persistent arrays. 5th Coq workshop (CW2013), July 22, Rennes, France View slides (pdf)
Computable refinements by quotients and parametricity. 19th Types for proofs and programs meeting (TYPES2013), April 22-26, Toulouse, France View slides (pdf)
2012
Verifying computer algebra algorithms: refinements and automation to the rescue. Mathematics Algorithms and Proofs 2012 (MAP2012), September 17-21, Universität Konstanz, Germany View slides (pdf)
A refinement-based approach to computational algebra in Coq. Third International Conference on Interactive Theorem Proving (ITP2012), August 13-15, Princeton, USA View slides (pdf)
Experience report on computation inside Coq. Coq workshop 2012 (CW2012), Princeton, USA View slides (pdf)
Effective algebra with Coq and SSReflect. May 2012, MSR-INRIA Joint Center, Saclay, France
2011
Full reduction at full throttle. First International Conference on Certified Programs and Proofs (CPP2011), Kenting, Tawain.
Effective algebra with Coq and SSReflect. October 2011, ENS Lyon, France.
Experiments with computable matrices in the Coq system. Coq workshop 2011 (CW2011), Berg en Dal, Netherlands.
2010
Experiments towards efficient computations in formalized linear algebra. Mathematics Algorithms and Proofs 2010 (MAP2010) , Logroño, Spain.