M. Beeson, “Mixing Computations and Proofs”, JFR, vol. 9, no. 1, pp. 71–99, Jan. 2016.