The goal was to automatize formal proofs of recurrence relations based on algorithms outputting (in most cases) a "certificate", computed by Maple and checked by Coq. This allowed us to combine the power of formal computation with the rigor of formal proof to prove results "soundly and quickly". We started a proof of Apery's theorem in this way, which is not finished to this date. My internship report (in English) is here.
Two-month internship with Eric Schost on the topic of matrix multiplication.The goal was to review existing algorithms, and possibly to implement some of the theoretical versions famous for their huge complexity on small matrices to get an idea.This was a fruitful idea as we discovered a way to build "practical" matrix product algorithms from Pan's algorithms. More details in the internship report..
Five month internship with Assia Mahboubi at Inria Saclay on the certification in Coq of numerical approximations of solutions of differential equations in Coq.The report.