# Talks

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)
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)
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)
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
Full reduction at full throttle.

*First International Conference on Certified Programs and Proofs (CPP2011)*, Kenting, Tawain. View slides (pdf)
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. View slides (pdf)
Experiments towards efficient computations in formalized linear algebra.

*Mathematics Algorithms and Proofs 2010 (MAP2010)*, Logroño, Spain. View slides (pdf)