R. W. Butler, “Formalization of the Integral Calculus in the PVS Theorem Prover”, JFR, vol. 2, no. 1, pp. 1–26, Jan. 2009.