Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
By Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
By Christoph Koutschan
Creative telescoping for D-finite functions - Lecture 2
By Christoph Koutschan
Appears in collection : 2014 - T2 - Semantics of proofs and certified mathematics
Georges Gonthier (Microsoft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau): Digitizing the Group Theory of the Odd Order Theorem