Wenda Li, Lawrence C. Paulson: Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. CPP 2019: 52-64