Bagnall, A.; Stewart, G. Certifying the True Error: Machine Learning in Coq With Verified Generalization Guarantees. AAAI 2019, 33, 2662-2669.