Program extraction in constructive analysis

Helmut Schwichtenberg

pp. 255-275

in: Erik Palmgren, Krister Segerberg (eds), Logicism, intuitionism, and formalism, Berlin, Springer, 2009

Abstract

We sketch a development of constructive analysis in Bishop's style, with special emphasis on low type-level witnesses (using separability of the reals). The goal is to set up things in such a way that realistically executable programs can be extracted from proofs. This is carried out for (1) the Intermediate Value Theorem and (2) the existence of a continuous inverse to a monotonically increasing continuous function. Using the Minlog proof assistant, the proofs leading to the Intermediate Value Theorem are formalized and realizing terms extracted. It turns out that evaluating these terms is a reasonably fast algorithm to compute, say, approximations of √2.