Proofs-as-Programs in Computable Analysis
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.
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.23.332
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.23.332.308
Hosted By Universitätsbibliothek TU Berlin.