Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
By Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
By Christoph Koutschan
Appears in collections : Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certification, Exposés de recherche
In this talk, we are going to show on some elementary examples how computation can easily be incorporated inside proof in a proof system like Coq.