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