Proofs-as-Programs in Computable Analysis
Ulrich Berger · 2024
Since the work of Brouwer, Kolmogorov, Goedel, Kleene and many others we know that constructive proofs have computational meaning. In Computer Science this idea is known as the "proofs-as-programs paradigm" or "Curry-Howard correspondence". We present examples from computable analysis showing that this paradigm not only works in principle, but can be used to automatically synthesise practically relevant certified programs.