Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
De Christoph Koutschan
Apparaît dans les 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.