Our goal is to design efficient computer-algebra algorithms and certify computer-algebra calculations by formalizing algorithmic mathematical theories in the proof assistant Coq, in the specific context of special-functions applications.
This INRIA team is located on the campus of École Polytechnique, as part of the Saclay – Île-de-France INRIA Research Center. It was formerly involved in the Microsoft Research – Inria Joint Centre, in the projects Dynamic Dictionary of Mathematical Functions (DDMF) and Mathematical Components.
Former members and long-term visitors:
Annoucements for the seminar “Computations and Proofs” will appear here. You can also subscribe to the annoucements.
Our list of publications is available through the French archive HAL (generated list).
A few potential internships descriptions are available here.