Berger, U. Proofs-As-Programs in Computable Analysis. eceasst 2009, 23.