Phenomenological Reviews

Series | Book | Chapter

182104

Program extraction in constructive analysis

Helmut Schwichtenberg

pp. 255-275

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.

Publication details

Published in:

Palmgren Erik, Segerberg Krister (2009) Logicism, intuitionism, and formalism: what has become of them?. Dordrecht, Springer.

Pages: 255-275

DOI: 10.1007/978-1-4020-8926-8_13

Full citation:

Schwichtenberg Helmut (2009) „Program extraction in constructive analysis“, In: E. Palmgren & K. Segerberg (eds.), Logicism, intuitionism, and formalism, Dordrecht, Springer, 255–275.