Proofs-as-Programs in Computable Analysis - Berger, Ulrich (Electronic Communications of the EASST, 2009)
Since the work of Brouwer, Kolmogorov, Goedel, Kleene and many otherswe know that constructive proofs have computational meaning. InComputer Science this idea is known as the"proofs-as-programs paradigm" or "Curry-Howard correspondence". We present examples from computable analysis showing that thisparadigm not only works in principle, but can be used to automaticallysynthesise practically relevant certified programs.