Proofs-as-Programs in Computable Analysis

Authors

  • Ulrich Berger

DOI:

https://doi.org/10.14279/tuj.eceasst.23.332

Abstract

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.

Downloads

Published

2009-12-17

How to Cite

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