U. Berger, “Proofs-as-Programs in Computable Analysis”, ECEASST, vol. 23, Dec. 2009.