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 is 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, complete from 2013 on, is available through the French archive HAL (generated list).
A few potential internships descriptions are available here.